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  4468  sotritrieq  4470  en2lp  4701  poxp  6468  nntri2  6767  finexdc  7207  elssdc  7209  unfidisj  7229  fidcenumlemrks  7270  pw1nel3  7590  sucpw1nel3  7592  onntri45  7600  aptipr  8008  lttri3  8405  letr  8408  apirr  8935  apti  8952  elnnz  9658  xrlttri3  10209  xrletr  10220  exp3val  10991  bcval4  11204  hashunlem  11258  maxleast  11994  xrmaxlesup  12041  lcmval  12857  lcmcllem  12861  lcmgcdlem  12871  isprm3  12912  pcpremul  13092  ivthinc  15793  lgsdir2  16250  2lgslem3  16318  structiedg0val  16379  vtxd0nedgbfi  16638  vdegp1aid  16653  bj-nnor  16860  pwtrufal  17125  pwle2  17126