Theorem ioran 764

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 793, anordc 969, or ianordc 911. 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 750	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 751	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 306	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 636	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 110	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 636	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 728	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 636	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 104   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.56  792  nnexmid  862  dcor  948  3ioran  1024  3ori  1341  ecase2d  1392  unssdif  3466  difundi  3483  dcun  3637  sotricim  4468  sotritrieq  4470  en2lp  4701  poxp  6468  nntri2  6767  finexdc  7207  elssdc  7209  unfidisj  7229  fidcenumlemrks  7270  pw1nel3  7591  sucpw1nel3  7593  onntri45  7601  aptipr  8009  lttri3  8406  letr  8409  apirr  8936  apti  8953  elnnz  9659  xrlttri3  10210  xrletr  10221  exp3val  10993  bcval4  11206  hashunlem  11260  maxleast  11996  xrmaxlesup  12044  lcmval  12860  lcmcllem  12864  lcmgcdlem  12874  isprm3  12915  pcpremul  13095  ivthinc  15835  lgsdir2  16318  2lgslem3  16386  structiedg0val  16447  vtxd0nedgbfi  16706  vdegp1aid  16721  bj-nnor  16928  pwtrufal  17193  pwle2  17194