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

Theorem ioran 726
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 755, anordc 925, or ianordc 869. 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 712 . . 3 (¬ (𝜑𝜓) → ¬ 𝜑)
2 pm2.46 713 . . 3 (¬ (𝜑𝜓) → ¬ 𝜓)
31, 2jca 304 . 2 (¬ (𝜑𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4 simpl 108 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
54con2i 601 . . . 4 (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6 simpr 109 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
76con2i 601 . . . 4 (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
85, 7jaoi 690 . . 3 ((𝜑𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
98con2i 601 . 2 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
103, 9impbii 125 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 103  wb 104  wo 682
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 588  ax-in2 589  ax-io 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm4.56  754  nnexmid  820  dcor  904  3ioran  962  3ori  1263  unssdif  3281  difundi  3298  dcun  3443  sotricim  4215  sotritrieq  4217  en2lp  4439  poxp  6097  nntri2  6358  finexdc  6764  unfidisj  6778  fidcenumlemrks  6809  aptipr  7417  lttri3  7812  letr  7815  apirr  8335  apti  8352  elnnz  9032  xrlttri3  9551  xrletr  9559  exp3val  10263  bcval4  10466  hashunlem  10518  maxleast  10953  xrmaxlesup  10996  lcmval  11671  lcmcllem  11675  lcmgcdlem  11685  isprm3  11726  ivthinc  12717  bj-nnor  12873  pwtrufal  13119  pwle2  13120
  Copyright terms: Public domain W3C validator