Theorem pm4.56 988

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397   ∨ wo 846

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 206  df-an 398  df-or 847

This theorem is referenced by:  oran  989  neanior  3036  rexprg  4701  prneimg  4856  ord1eln01  8496  ord2eln012  8497  unfi  9172  ssxr  11283  isirred2  20235  aaliou3lem9  25863  mideulem2  27985  opphllem  27986  bj-dfbi4  35450  topdifinffinlem  36228  icorempo  36232  dalawlem13  38754  cdleme22b  39212  aks6d1c2p2  40957  metakunt1  40985  negn0nposznnd  41194  jm2.26lem3  41740  wopprc  41769  iunconnlem2  43696  icccncfext  44603  cncfiooicc  44610  fourierdlem25  44848  fourierdlem35  44858  fourierswlem  44946  fouriersw  44947  etransclem44  44994  sge0split  45125  islininds2  47165  digexp  47293