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  3025  rexprg  4654  prneimg  4810  ord1eln01  8423  ord2eln012  8424  unfi  9095  ssxr  11202  isirred2  20357  aaliou3lem9  26314  mideulem2  28806  opphllem  28807  weiunfr  36661  bj-dfbi4  36773  topdifinffinlem  37552  icorempo  37556  dalawlem13  40143  cdleme22b  40601  aks6d1c2p2  42373  negn0nposznnd  42537  jm2.26lem3  43243  wopprc  43272  iunconnlem2  45175  icccncfext  46131  cncfiooicc  46138  fourierdlem25  46376  fourierdlem35  46386  fourierswlem  46474  fouriersw  46475  etransclem44  46522  sge0split  46653  islininds2  48730  digexp  48853