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 395   ∨ 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 396  df-or 844

This theorem is referenced by:  oran  986  nornotOLD  1527  neanior  3036  rexprg  4629  prneimg  4782  unfi  8917  ssxr  10975  isirred2  19858  aaliou3lem9  25415  mideulem2  26999  opphllem  27000  bj-dfbi4  34681  topdifinffinlem  35445  icorempo  35449  dalawlem13  37824  cdleme22b  38282  metakunt1  40053  negn0nposznnd  40231  jm2.26lem3  40739  wopprc  40768  iunconnlem2  42444  icccncfext  43318  cncfiooicc  43325  fourierdlem25  43563  fourierdlem35  43573  fourierswlem  43661  fouriersw  43662  etransclem44  43709  sge0split  43837  islininds2  45713  digexp  45841