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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  oran  1005  neanior  3051  rexprg  4664  prneimg  4820  ord1eln01  8482  ord2eln012  8483  unfi  9156  ssxr  11280  isirred2  20504  aaliou3lem9  26494  mideulem2  28996  opphllem  28997  weiunfr  36959  bj-dfbi4  37147  topdifinffinlem  37974  icorempo  37978  dalawlem13  40638  cdleme22b  41096  aks6d1c2p2  42867  negn0nposznnd  43024  jm2.26lem3  43711  wopprc  43740  iunconnlem2  45626  icccncfext  46584  cncfiooicc  46591  fourierdlem25  46829  fourierdlem35  46839  fourierswlem  46927  fouriersw  46928  etransclem44  46975  sge0split  47106  islininds2  49247  digexp  49370