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  3033  rexprg  4702  prneimg  4859  ord1eln01  8533  ord2eln012  8534  unfi  9210  ssxr  11328  isirred2  20438  aaliou3lem9  26407  mideulem2  28757  opphllem  28758  weiunfr  36450  bj-dfbi4  36556  topdifinffinlem  37330  icorempo  37334  dalawlem13  39866  cdleme22b  40324  aks6d1c2p2  42101  metakunt1  42187  negn0nposznnd  42296  jm2.26lem3  42990  wopprc  43019  iunconnlem2  44933  icccncfext  45843  cncfiooicc  45850  fourierdlem25  46088  fourierdlem35  46098  fourierswlem  46186  fouriersw  46187  etransclem44  46234  sge0split  46365  islininds2  48330  digexp  48457