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  4050  sotritrieq  4052  en2lp  4231  poxp  5791  nntri2  6005  aptipr  6603  lttri3  6847  letr  6850  apirr  7341  apti  7358  elnnz  7981  xrlttri3  8436  xrletr  8442  nnexmid  8833
  Copyright terms: Public domain W3C validator