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

Theorem ioran 702
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 841, anordc 898, or ianordc 833. 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 690 . . 3 (¬ (𝜑𝜓) → ¬ 𝜑)
2 pm2.46 691 . . 3 (¬ (𝜑𝜓) → ¬ 𝜓)
31, 2jca 300 . 2 (¬ (𝜑𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4 simpl 107 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
54con2i 590 . . . 4 (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6 simpr 108 . . . . 5 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
76con2i 590 . . . 4 (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
85, 7jaoi 669 . . 3 ((𝜑𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
98con2i 590 . 2 ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑𝜓))
103, 9impbii 124 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 102  wb 103  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm4.56  840  dcor  877  3ioran  935  3ori  1232  unssdif  3217  difundi  3234  sotricim  4113  sotritrieq  4115  en2lp  4332  poxp  5930  nntri2  6185  finexdc  6543  unfidisj  6557  aptipr  7101  lttri3  7466  letr  7469  apirr  7980  apti  7997  elnnz  8654  xrlttri3  9160  xrletr  9166  expival  9792  bcval4  9993  hashunlem  10045  maxleast  10471  lcmval  10823  lcmcllem  10827  lcmgcdlem  10837  isprm3  10878  nnexmid  11001
  Copyright terms: Public domain W3C validator