Theorem ioran 759

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 788, anordc 964, or ianordc 906. 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 745	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 746	. . 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 723	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 632	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  787  nnexmid  857  dcor  943  3ioran  1019  3ori  1336  ecase2d  1387  unssdif  3442  difundi  3459  dcun  3604  sotricim  4420  sotritrieq  4422  en2lp  4652  poxp  6397  nntri2  6662  finexdc  7092  elssdc  7094  unfidisj  7114  fidcenumlemrks  7152  pw1nel3  7449  sucpw1nel3  7451  onntri45  7459  aptipr  7861  lttri3  8259  letr  8262  apirr  8785  apti  8802  elnnz  9489  xrlttri3  10032  xrletr  10043  exp3val  10804  bcval4  11015  hashunlem  11068  maxleast  11791  xrmaxlesup  11837  lcmval  12653  lcmcllem  12657  lcmgcdlem  12667  isprm3  12708  pcpremul  12884  ivthinc  15386  lgsdir2  15781  2lgslem3  15849  structiedg0val  15910  vtxd0nedgbfi  16169  vdegp1aid  16184  bj-nnor  16381  pwtrufal  16649  pwle2  16650