Theorem pm4.56 990

Description: Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm4.56	⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

Proof of Theorem pm4.56

Step	Hyp	Ref	Expression
1		ioran 985	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2	1	bicomi 224	1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848

This theorem is referenced by:  oran  991  neanior  3026  rexprg  4678  prneimg  4835  ord1eln01  8513  ord2eln012  8514  unfi  9190  ssxr  11309  isirred2  20386  aaliou3lem9  26315  mideulem2  28718  opphllem  28719  weiunfr  36490  bj-dfbi4  36596  topdifinffinlem  37370  icorempo  37374  dalawlem13  39907  cdleme22b  40365  aks6d1c2p2  42137  negn0nposznnd  42300  jm2.26lem3  43000  wopprc  43029  iunconnlem2  44934  icccncfext  45896  cncfiooicc  45903  fourierdlem25  46141  fourierdlem35  46151  fourierswlem  46239  fouriersw  46240  etransclem44  46287  sge0split  46418  islininds2  48440  digexp  48567