Theorem ioran 760

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 789, anordc 965, or ianordc 907. 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 746	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 747	. . 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 724	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 632	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  788  nnexmid  858  dcor  944  3ioran  1020  3ori  1337  ecase2d  1388  unssdif  3456  difundi  3473  dcun  3619  sotricim  4444  sotritrieq  4446  en2lp  4676  poxp  6428  nntri2  6727  finexdc  7160  elssdc  7162  unfidisj  7182  fidcenumlemrks  7223  pw1nel3  7541  sucpw1nel3  7543  onntri45  7551  aptipr  7956  lttri3  8353  letr  8356  apirr  8879  apti  8896  elnnz  9587  xrlttri3  10130  xrletr  10141  exp3val  10903  bcval4  11114  hashunlem  11168  maxleast  11898  xrmaxlesup  11944  lcmval  12760  lcmcllem  12764  lcmgcdlem  12774  isprm3  12815  pcpremul  12991  ivthinc  15508  lgsdir2  15906  2lgslem3  15974  structiedg0val  16035  vtxd0nedgbfi  16294  vdegp1aid  16309  bj-nnor  16506  pwtrufal  16771  pwle2  16772