Theorem pm4.56 990

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 848

This theorem is referenced by:  oran  991  neanior  3018  rexprg  4661  prneimg  4818  ord1eln01  8460  ord2eln012  8461  unfi  9135  ssxr  11243  isirred2  20330  aaliou3lem9  26258  mideulem2  28661  opphllem  28662  weiunfr  36455  bj-dfbi4  36561  topdifinffinlem  37335  icorempo  37339  dalawlem13  39877  cdleme22b  40335  aks6d1c2p2  42107  negn0nposznnd  42270  jm2.26lem3  42990  wopprc  43019  iunconnlem2  44924  icccncfext  45885  cncfiooicc  45892  fourierdlem25  46130  fourierdlem35  46140  fourierswlem  46228  fouriersw  46229  etransclem44  46276  sge0split  46407  islininds2  48473  digexp  48596