Theorem ioran 742

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 771, anordc 946, or ianordc 889. 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 728	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 729	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 304	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 108	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 617	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 617	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 706	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 617	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 125	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.56  770  nnexmid  840  dcor  925  3ioran  983  3ori  1290  unssdif  3356  difundi  3373  dcun  3518  sotricim  4300  sotritrieq  4302  en2lp  4530  poxp  6196  nntri2  6458  finexdc  6864  unfidisj  6883  fidcenumlemrks  6914  pw1nel3  7183  sucpw1nel3  7185  onntri45  7193  aptipr  7578  lttri3  7974  letr  7977  apirr  8499  apti  8516  elnnz  9197  xrlttri3  9729  xrletr  9740  exp3val  10453  bcval4  10661  hashunlem  10713  maxleast  11151  xrmaxlesup  11196  lcmval  11991  lcmcllem  11995  lcmgcdlem  12005  isprm3  12046  pcpremul  12221  ivthinc  13221  lgsdir2  13534  bj-nnor  13575  pwtrufal  13837  pwle2  13838