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  3053  rexprg  4665  prneimg  4821  ord1eln01  8483  ord2eln012  8484  unfi  9158  ssxr  11290  isirred2  20528  aaliou3lem9  26542  mideulem2  29044  opphllem  29045  weiunfr  37011  bj-dfbi4  37199  topdifinffinlem  38026  icorempo  38030  dalawlem13  40690  cdleme22b  41148  aks6d1c2p2  42919  negn0nposznnd  43076  jm2.26lem3  43761  wopprc  43790  iunconnlem2  45676  icccncfext  46634  cncfiooicc  46641  fourierdlem25  46879  fourierdlem35  46889  fourierswlem  46977  fouriersw  46978  etransclem44  47025  sge0split  47156  islininds2  49297  digexp  49420