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  6396  nntri2  6661  finexdc  7091  elssdc  7093  unfidisj  7113  fidcenumlemrks  7151  pw1nel3  7448  sucpw1nel3  7450  onntri45  7458  aptipr  7860  lttri3  8258  letr  8261  apirr  8784  apti  8801  elnnz  9488  xrlttri3  10031  xrletr  10042  exp3val  10802  bcval4  11013  hashunlem  11066  maxleast  11773  xrmaxlesup  11819  lcmval  12634  lcmcllem  12638  lcmgcdlem  12648  isprm3  12689  pcpremul  12865  ivthinc  15366  lgsdir2  15761  2lgslem3  15829  structiedg0val  15890  vtxd0nedgbfi  16149  vdegp1aid  16164  bj-nnor  16330  pwtrufal  16598  pwle2  16599