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

Theorem ioran 741
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 770, anordc 940, or ianordc 884. 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 727 . . 3 (¬ (𝜑𝜓) → ¬ 𝜑)
2 pm2.46 728 . . 3 (¬ (𝜑𝜓) → ¬ 𝜓)
31, 2jca 304 . 2 (¬ (𝜑𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4 simpl 108 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
54con2i 616 . . . 4 (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6 simpr 109 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
76con2i 616 . . . 4 (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
85, 7jaoi 705 . . 3 ((𝜑𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
98con2i 616 . 2 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
103, 9impbii 125 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 103  wb 104  wo 697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.56  769  nnexmid  835  dcor  919  3ioran  977  3ori  1278  unssdif  3306  difundi  3323  dcun  3468  sotricim  4240  sotritrieq  4242  en2lp  4464  poxp  6122  nntri2  6383  finexdc  6789  unfidisj  6803  fidcenumlemrks  6834  aptipr  7442  lttri3  7837  letr  7840  apirr  8360  apti  8377  elnnz  9057  xrlttri3  9576  xrletr  9584  exp3val  10288  bcval4  10491  hashunlem  10543  maxleast  10978  xrmaxlesup  11021  lcmval  11733  lcmcllem  11737  lcmgcdlem  11747  isprm3  11788  ivthinc  12779  bj-nnor  12935  pwtrufal  13181  pwle2  13182
  Copyright terms: Public domain W3C validator