Theorem ioran 757

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 786, anordc 962, or ianordc 904. 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 743	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 744	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 306	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 630	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 110	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 630	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 721	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 630	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 617  ax-in2 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  785  nnexmid  855  dcor  941  3ioran  1017  3ori  1334  ecase2d  1385  unssdif  3439  difundi  3456  dcun  3601  sotricim  4414  sotritrieq  4416  en2lp  4646  poxp  6384  nntri2  6648  finexdc  7073  elssdc  7075  unfidisj  7095  fidcenumlemrks  7131  pw1nel3  7427  sucpw1nel3  7429  onntri45  7437  aptipr  7839  lttri3  8237  letr  8240  apirr  8763  apti  8780  elnnz  9467  xrlttri3  10005  xrletr  10016  exp3val  10775  bcval4  10986  hashunlem  11038  maxleast  11739  xrmaxlesup  11785  lcmval  12600  lcmcllem  12604  lcmgcdlem  12614  isprm3  12655  pcpremul  12831  ivthinc  15332  lgsdir2  15727  2lgslem3  15795  structiedg0val  15856  bj-nnor  16153  pwtrufal  16422  pwle2  16423