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  3111  prneimg  4787  ssxr  10712  isirred2  19453  aaliou3lem9  24941  mideulem2  26522  opphllem  26523  bj-dfbi4  33908  topdifinffinlem  34630  icorempo  34634  dalawlem13  37021  cdleme22b  37479  negn0nposznnd  39175  jm2.26lem3  39605  wopprc  39634  iunconnlem2  41276  icccncfext  42177  cncfiooicc  42184  fourierdlem25  42424  fourierdlem35  42434  fourierswlem  42522  fouriersw  42523  etransclem44  42570  sge0split  42698  islininds2  44546  digexp  44674