Theorem pm4.56 1001

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  oran  1002  neanior  3049  rexprg  4653  prneimg  4809  ord1eln01  8459  ord2eln012  8460  unfi  9133  ssxr  11246  isirred2  20457  aaliou3lem9  26402  mideulem2  28891  opphllem  28892  weiunfr  36788  bj-dfbi4  36977  topdifinffinlem  37802  icorempo  37806  dalawlem13  40468  cdleme22b  40926  aks6d1c2p2  42697  negn0nposznnd  42852  jm2.26lem3  43539  wopprc  43568  iunconnlem2  45471  icccncfext  46422  cncfiooicc  46429  fourierdlem25  46667  fourierdlem35  46677  fourierswlem  46765  fouriersw  46766  etransclem44  46813  sge0split  46944  islininds2  49067  digexp  49190