Theorem pm4.56 1004

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  oran  1005  neanior  3048  rexprg  4654  prneimg  4808  ord1eln01  8508  ord2eln012  8509  unfi  9190  ssxr  11383  isirred2  20657  aaliou3lem9  26683  mideulem2  29216  opphllem  29217  weiunfr  37348  bj-dfbi4  37536  topdifinffinlem  38364  icorempo  38368  dalawlem13  41034  cdleme22b  41492  aks6d1c2p2  43263  negn0nposznnd  43433  jm2.26lem3  44102  wopprc  44131  iunconnlem2  46011  icccncfext  46991  cncfiooicc  46998  fourierdlem25  47236  fourierdlem35  47246  fourierswlem  47334  fouriersw  47335  etransclem44  47382  sge0split  47513  islininds2  49690  digexp  49813