Theorem pm4.56 991

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

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

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 849

This theorem is referenced by:  oran  992  neanior  3026  rexprg  4656  prneimg  4812  ord1eln01  8433  ord2eln012  8434  unfi  9107  ssxr  11214  isirred2  20369  aaliou3lem9  26326  mideulem2  28818  opphllem  28819  weiunfr  36680  bj-dfbi4  36795  topdifinffinlem  37599  icorempo  37603  dalawlem13  40256  cdleme22b  40714  aks6d1c2p2  42486  negn0nposznnd  42649  jm2.26lem3  43355  wopprc  43384  iunconnlem2  45287  icccncfext  46242  cncfiooicc  46249  fourierdlem25  46487  fourierdlem35  46497  fourierswlem  46585  fouriersw  46586  etransclem44  46633  sge0split  46764  islininds2  48841  digexp  48964