Theorem ioran 757

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 786, anordc 962, or ianordc 904. 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 743	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 744	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 306	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 630	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 110	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 630	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 721	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 630	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 617  ax-in2 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  785  nnexmid  855  dcor  941  3ioran  1017  3ori  1334  ecase2d  1385  unssdif  3440  difundi  3457  dcun  3602  sotricim  4416  sotritrieq  4418  en2lp  4648  poxp  6390  nntri2  6655  finexdc  7083  elssdc  7085  unfidisj  7105  fidcenumlemrks  7141  pw1nel3  7437  sucpw1nel3  7439  onntri45  7447  aptipr  7849  lttri3  8247  letr  8250  apirr  8773  apti  8790  elnnz  9477  xrlttri3  10020  xrletr  10031  exp3val  10791  bcval4  11002  hashunlem  11054  maxleast  11761  xrmaxlesup  11807  lcmval  12622  lcmcllem  12626  lcmgcdlem  12636  isprm3  12677  pcpremul  12853  ivthinc  15354  lgsdir2  15749  2lgslem3  15817  structiedg0val  15878  vtxd0nedgbfi  16101  bj-nnor  16240  pwtrufal  16508  pwle2  16509