Theorem pm4.56 1004

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  oran  1005  neanior  3052  rexprg  4659  prneimg  4814  ord1eln01  8542  ord2eln012  8543  unfi  9224  ssxr  11418  isirred2  20702  aaliou3lem9  26734  mideulem2  29267  opphllem  29268  weiunfr  37470  bj-dfbi4  37658  topdifinffinlem  38538  icorempo  38542  dalawlem13  41206  cdleme22b  41664  aks6d1c2p2  43435  negn0nposznnd  43605  jm2.26lem3  44274  wopprc  44303  iunconnlem2  46177  icccncfext  47170  cncfiooicc  47177  fourierdlem25  47415  fourierdlem35  47425  fourierswlem  47513  fouriersw  47514  etransclem44  47561  sge0split  47692  islininds2  49927  digexp  50050