Theorem ioran 747

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 776, anordc 951, or ianordc 894. 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 733	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 734	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 304	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 108	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 622	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 622	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 711	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 622	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 125	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 609  ax-in2 610  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.56  775  nnexmid  845  dcor  930  3ioran  988  3ori  1295  unssdif  3362  difundi  3379  dcun  3525  sotricim  4308  sotritrieq  4310  en2lp  4538  poxp  6211  nntri2  6473  finexdc  6880  unfidisj  6899  fidcenumlemrks  6930  pw1nel3  7208  sucpw1nel3  7210  onntri45  7218  aptipr  7603  lttri3  7999  letr  8002  apirr  8524  apti  8541  elnnz  9222  xrlttri3  9754  xrletr  9765  exp3val  10478  bcval4  10686  hashunlem  10739  maxleast  11177  xrmaxlesup  11222  lcmval  12017  lcmcllem  12021  lcmgcdlem  12031  isprm3  12072  pcpremul  12247  ivthinc  13415  lgsdir2  13728  bj-nnor  13769  pwtrufal  14030  pwle2  14031