Theorem pm4.56 990

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  oran  991  neanior  3018  rexprg  4651  prneimg  4808  ord1eln01  8421  ord2eln012  8422  unfi  9095  ssxr  11203  isirred2  20324  aaliou3lem9  26274  mideulem2  28697  opphllem  28698  weiunfr  36440  bj-dfbi4  36546  topdifinffinlem  37320  icorempo  37324  dalawlem13  39862  cdleme22b  40320  aks6d1c2p2  42092  negn0nposznnd  42255  jm2.26lem3  42974  wopprc  43003  iunconnlem2  44908  icccncfext  45869  cncfiooicc  45876  fourierdlem25  46114  fourierdlem35  46124  fourierswlem  46212  fouriersw  46213  etransclem44  46260  sge0split  46391  islininds2  48470  digexp  48593