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  3023  rexprg  4631  prneimg  4787  ord1eln01  8420  ord2eln012  8421  unfi  9094  ssxr  11204  isirred2  20390  aaliou3lem9  26304  mideulem2  28790  opphllem  28791  weiunfr  36637  bj-dfbi4  36826  topdifinffinlem  37651  icorempo  37655  dalawlem13  40317  cdleme22b  40775  aks6d1c2p2  42546  negn0nposznnd  42702  jm2.26lem3  43417  wopprc  43446  iunconnlem2  45349  icccncfext  46303  cncfiooicc  46310  fourierdlem25  46548  fourierdlem35  46558  fourierswlem  46646  fouriersw  46647  etransclem44  46694  sge0split  46825  islininds2  48948  digexp  49071