Theorem ioran 705

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 846, anordc 903, or ianordc 838. 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 693	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 694	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 301	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 108	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 593	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 593	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 672	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 593	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 125	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   ∨ wo 665

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.56  845  dcor  882  3ioran  940  3ori  1237  unssdif  3237  difundi  3254  dcun  3398  sotricim  4161  sotritrieq  4163  en2lp  4385  poxp  6013  nntri2  6271  finexdc  6674  unfidisj  6688  fidcenumlemrks  6718  aptipr  7263  lttri3  7628  letr  7631  apirr  8145  apti  8162  elnnz  8823  xrlttri3  9330  xrletr  9336  exp3val  10020  bcval4  10223  hashunlem  10275  maxleast  10709  lcmval  11386  lcmcllem  11390  lcmgcdlem  11400  isprm3  11441  nnexmid  11964