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 226	1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   ∨ 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 209  df-an 399  df-or 844

This theorem is referenced by:  oran  986  nornotOLD  1525  neanior  3109  prneimg  4785  ssxr  10710  isirred2  19451  aaliou3lem9  24939  mideulem2  26520  opphllem  26521  bj-dfbi4  33906  topdifinffinlem  34631  icorempo  34635  dalawlem13  37034  cdleme22b  37492  negn0nposznnd  39188  jm2.26lem3  39618  wopprc  39647  iunconnlem2  41289  icccncfext  42190  cncfiooicc  42197  fourierdlem25  42437  fourierdlem35  42447  fourierswlem  42535  fouriersw  42536  etransclem44  42583  sge0split  42711  islininds2  44559  digexp  44687