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  3025  rexprg  4641  prneimg  4797  ord1eln01  8431  ord2eln012  8432  unfi  9105  ssxr  11215  isirred2  20401  aaliou3lem9  26316  mideulem2  28802  opphllem  28803  weiunfr  36649  bj-dfbi4  36838  topdifinffinlem  37663  icorempo  37667  dalawlem13  40329  cdleme22b  40787  aks6d1c2p2  42558  negn0nposznnd  42714  jm2.26lem3  43429  wopprc  43458  iunconnlem2  45361  icccncfext  46315  cncfiooicc  46322  fourierdlem25  46560  fourierdlem35  46570  fourierswlem  46658  fouriersw  46659  etransclem44  46706  sge0split  46837  islininds2  48960  digexp  49083