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  3024  rexprg  4677  prneimg  4834  ord1eln01  8516  ord2eln012  8517  unfi  9193  ssxr  11312  isirred2  20390  aaliou3lem9  26329  mideulem2  28679  opphllem  28680  weiunfr  36443  bj-dfbi4  36549  topdifinffinlem  37323  icorempo  37327  dalawlem13  39860  cdleme22b  40318  aks6d1c2p2  42095  metakunt1  42181  negn0nposznnd  42296  jm2.26lem3  42991  wopprc  43020  iunconnlem2  44927  icccncfext  45874  cncfiooicc  45881  fourierdlem25  46119  fourierdlem35  46129  fourierswlem  46217  fouriersw  46218  etransclem44  46265  sge0split  46396  islininds2  48374  digexp  48501