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

Theorem ioran 705
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 846, anordc 903, or ianordc 838. 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 693 . . 3 (¬ (𝜑𝜓) → ¬ 𝜑)
2 pm2.46 694 . . 3 (¬ (𝜑𝜓) → ¬ 𝜓)
31, 2jca 301 . 2 (¬ (𝜑𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4 simpl 108 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
54con2i 593 . . . 4 (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6 simpr 109 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
76con2i 593 . . . 4 (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
85, 7jaoi 672 . . 3 ((𝜑𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
98con2i 593 . 2 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
103, 9impbii 125 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 103  wb 104  wo 665
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.56  845  dcor  882  3ioran  940  3ori  1237  unssdif  3237  difundi  3254  dcun  3398  sotricim  4161  sotritrieq  4163  en2lp  4385  poxp  6013  nntri2  6271  finexdc  6674  unfidisj  6688  fidcenumlemrks  6718  aptipr  7263  lttri3  7628  letr  7631  apirr  8145  apti  8162  elnnz  8823  xrlttri3  9330  xrletr  9336  exp3val  10020  bcval4  10223  hashunlem  10275  maxleast  10709  lcmval  11386  lcmcllem  11390  lcmgcdlem  11400  isprm3  11441  nnexmid  11964
  Copyright terms: Public domain W3C validator