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  4642  prneimg  4798  ord1eln01  8424  ord2eln012  8425  unfi  9098  ssxr  11206  isirred2  20392  aaliou3lem9  26327  mideulem2  28816  opphllem  28817  weiunfr  36665  bj-dfbi4  36854  topdifinffinlem  37677  icorempo  37681  dalawlem13  40343  cdleme22b  40801  aks6d1c2p2  42572  negn0nposznnd  42728  jm2.26lem3  43447  wopprc  43476  iunconnlem2  45379  icccncfext  46333  cncfiooicc  46340  fourierdlem25  46578  fourierdlem35  46588  fourierswlem  46676  fouriersw  46677  etransclem44  46724  sge0split  46855  islininds2  48972  digexp  49095