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  3048  rexprg  4658  prneimg  4814  ord1eln01  8483  ord2eln012  8484  unfi  9165  ssxr  11303  isirred2  20562  aaliou3lem9  26586  mideulem2  29089  opphllem  29090  weiunfr  37086  bj-dfbi4  37274  topdifinffinlem  38101  icorempo  38105  dalawlem13  40756  cdleme22b  41214  aks6d1c2p2  42985  negn0nposznnd  43157  jm2.26lem3  43842  wopprc  43871  iunconnlem2  45757  icccncfext  46715  cncfiooicc  46722  fourierdlem25  46960  fourierdlem35  46970  fourierswlem  47058  fouriersw  47059  etransclem44  47106  sge0split  47237  islininds2  49414  digexp  49537