Theorem ioran 753

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 782, anordc 958, or ianordc 900. 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 739	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 740	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 306	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 628	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 110	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 628	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 717	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 628	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 615  ax-in2 616  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  781  nnexmid  851  dcor  937  3ioran  995  3ori  1311  unssdif  3399  difundi  3416  dcun  3561  sotricim  4359  sotritrieq  4361  en2lp  4591  poxp  6299  nntri2  6561  finexdc  6972  unfidisj  6992  fidcenumlemrks  7028  pw1nel3  7316  sucpw1nel3  7318  onntri45  7326  aptipr  7727  lttri3  8125  letr  8128  apirr  8651  apti  8668  elnnz  9355  xrlttri3  9891  xrletr  9902  exp3val  10652  bcval4  10863  hashunlem  10915  maxleast  11397  xrmaxlesup  11443  lcmval  12258  lcmcllem  12262  lcmgcdlem  12272  isprm3  12313  pcpremul  12489  ivthinc  14987  lgsdir2  15382  2lgslem3  15450  bj-nnor  15488  pwtrufal  15752  pwle2  15753