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  3049  rexprg  4658  prneimg  4814  ord1eln01  8497  ord2eln012  8498  unfi  9179  ssxr  11372  isirred2  20644  aaliou3lem9  26670  mideulem2  29203  opphllem  29204  weiunfr  37235  bj-dfbi4  37423  topdifinffinlem  38250  icorempo  38254  dalawlem13  40920  cdleme22b  41378  aks6d1c2p2  43149  negn0nposznnd  43319  jm2.26lem3  43987  wopprc  44016  iunconnlem2  45902  icccncfext  46866  cncfiooicc  46873  fourierdlem25  47111  fourierdlem35  47121  fourierswlem  47209  fouriersw  47210  etransclem44  47257  sge0split  47388  islininds2  49565  digexp  49688