Theorem ioran 760

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 789, anordc 965, or ianordc 907. 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

Step	Hyp	Ref	Expression
1		pm2.45 746	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 747	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 306	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 632	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 110	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 632	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 724	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 632	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   ∨ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  788  nnexmid  858  dcor  944  3ioran  1020  3ori  1337  ecase2d  1388  unssdif  3460  difundi  3477  dcun  3623  sotricim  4449  sotritrieq  4451  en2lp  4681  poxp  6441  nntri2  6740  finexdc  7173  elssdc  7175  unfidisj  7195  fidcenumlemrks  7236  pw1nel3  7554  sucpw1nel3  7556  onntri45  7564  aptipr  7972  lttri3  8369  letr  8372  apirr  8896  apti  8913  elnnz  9604  xrlttri3  10149  xrletr  10160  exp3val  10927  bcval4  11139  hashunlem  11193  maxleast  11923  xrmaxlesup  11969  lcmval  12785  lcmcllem  12789  lcmgcdlem  12799  isprm3  12840  pcpremul  13016  ivthinc  15634  lgsdir2  16032  2lgslem3  16100  structiedg0val  16161  vtxd0nedgbfi  16420  vdegp1aid  16435  bj-nnor  16632  pwtrufal  16897  pwle2  16898