ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ioran Structured version   GIF version

Theorem ioran 668
Description: Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 806, anordc 862, or ianordc 798. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Assertion
Ref Expression
ioran (¬ (φ ψ) ↔ (¬ φ ¬ ψ))

Proof of Theorem ioran
StepHypRef Expression
1 pm2.45 656 . . 3 (¬ (φ ψ) → ¬ φ)
2 pm2.46 657 . . 3 (¬ (φ ψ) → ¬ ψ)
31, 2jca 290 . 2 (¬ (φ ψ) → (¬ φ ¬ ψ))
4 simpl 102 . . . . 5 ((¬ φ ¬ ψ) → ¬ φ)
54con2i 557 . . . 4 (φ → ¬ (¬ φ ¬ ψ))
6 simpr 103 . . . . 5 ((¬ φ ¬ ψ) → ¬ ψ)
76con2i 557 . . . 4 (ψ → ¬ (¬ φ ¬ ψ))
85, 7jaoi 635 . . 3 ((φ ψ) → ¬ (¬ φ ¬ ψ))
98con2i 557 . 2 ((¬ φ ¬ ψ) → ¬ (φ ψ))
103, 9impbii 117 1 (¬ (φ ψ) ↔ (¬ φ ¬ ψ))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   wa 97  wb 98   wo 628
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm4.56  805  dcor  842  3ioran  899  3ori  1194  unssdif  3166  difundi  3183  sotricim  4051  sotritrieq  4053  en2lp  4232  poxp  5794  nntri2  6012  aptipr  6613  lttri3  6895  letr  6898  apirr  7389  apti  7406  elnnz  8031  xrlttri3  8488  xrletr  8494  expival  8911  nnexmid  9234
  Copyright terms: Public domain W3C validator