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

Theorem ioran 669
 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 807, anordc 863, or ianordc 799. 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 657 . . 3 (¬ (𝜑𝜓) → ¬ 𝜑)
2 pm2.46 658 . . 3 (¬ (𝜑𝜓) → ¬ 𝜓)
31, 2jca 290 . 2 (¬ (𝜑𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4 simpl 102 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
54con2i 557 . . . 4 (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6 simpr 103 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
76con2i 557 . . . 4 (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
85, 7jaoi 636 . . 3 ((𝜑𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
98con2i 557 . 2 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
103, 9impbii 117 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ∧ wa 97   ↔ wb 98   ∨ wo 629 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 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  pm4.56  806  dcor  843  3ioran  900  3ori  1195  unssdif  3172  difundi  3189  sotricim  4060  sotritrieq  4062  en2lp  4278  poxp  5853  nntri2  6073  aptipr  6739  lttri3  7098  letr  7101  apirr  7596  apti  7613  elnnz  8255  xrlttri3  8718  xrletr  8724  expival  9257  nnexmid  9899
 Copyright terms: Public domain W3C validator