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  3444  difundi  3461  dcun  3606  sotricim  4426  sotritrieq  4428  en2lp  4658  poxp  6406  nntri2  6705  finexdc  7135  elssdc  7137  unfidisj  7157  fidcenumlemrks  7195  pw1nel3  7492  sucpw1nel3  7494  onntri45  7502  aptipr  7904  lttri3  8301  letr  8304  apirr  8827  apti  8844  elnnz  9533  xrlttri3  10076  xrletr  10087  exp3val  10849  bcval4  11060  hashunlem  11113  maxleast  11836  xrmaxlesup  11882  lcmval  12698  lcmcllem  12702  lcmgcdlem  12712  isprm3  12753  pcpremul  12929  ivthinc  15437  lgsdir2  15835  2lgslem3  15903  structiedg0val  15964  vtxd0nedgbfi  16223  vdegp1aid  16238  bj-nnor  16435  pwtrufal  16702  pwle2  16703