Theorem ioran 764

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 793, anordc 969, or ianordc 911. 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 750	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 751	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 306	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 636	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 110	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 636	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 728	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 636	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 104   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.56  792  nnexmid  862  dcor  948  3ioran  1024  3ori  1341  ecase2d  1392  unssdif  3466  difundi  3483  dcun  3637  sotricim  4470  sotritrieq  4472  en2lp  4703  poxp  6472  nntri2  6771  finexdc  7211  elssdc  7213  unfidisj  7233  fidcenumlemrks  7275  pw1nel3  7596  sucpw1nel3  7598  onntri45  7606  aptipr  8014  lttri3  8411  letr  8414  apirr  8941  apti  8958  elnnz  9665  xrlttri3  10216  xrletr  10227  exp3val  10999  bcval4  11212  hashunlem  11266  maxleast  12002  xrmaxlesup  12050  lcmval  12866  lcmcllem  12870  lcmgcdlem  12880  isprm3  12921  pcpremul  13101  ivthinc  15869  lgsdir2  16357  2lgslem3  16425  structiedg0val  16486  vtxd0nedgbfi  16745  vdegp1aid  16760  bj-nnor  16967  pwtrufal  17232  pwle2  17233