Theorem pm4.56 985

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 980	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2	1	bicomi 223	1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 394   ∨ wo 843

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 206  df-an 395  df-or 844

This theorem is referenced by:  oran  986  neanior  3033  rexprg  4701  prneimg  4856  ord1eln01  8500  ord2eln012  8501  unfi  9176  ssxr  11289  isirred2  20314  aaliou3lem9  26097  mideulem2  28250  opphllem  28251  bj-dfbi4  35755  topdifinffinlem  36533  icorempo  36537  dalawlem13  39059  cdleme22b  39517  aks6d1c2p2  41265  metakunt1  41293  negn0nposznnd  41498  jm2.26lem3  42044  wopprc  42073  iunconnlem2  44000  icccncfext  44903  cncfiooicc  44910  fourierdlem25  45148  fourierdlem35  45158  fourierswlem  45246  fouriersw  45247  etransclem44  45294  sge0split  45425  islininds2  47254  digexp  47382