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  3021  rexprg  4650  prneimg  4806  ord1eln01  8411  ord2eln012  8412  unfi  9080  ssxr  11182  isirred2  20340  aaliou3lem9  26286  mideulem2  28713  opphllem  28714  weiunfr  36507  bj-dfbi4  36613  topdifinffinlem  37387  icorempo  37391  dalawlem13  39928  cdleme22b  40386  aks6d1c2p2  42158  negn0nposznnd  42321  jm2.26lem3  43040  wopprc  43069  iunconnlem2  44973  icccncfext  45931  cncfiooicc  45938  fourierdlem25  46176  fourierdlem35  46186  fourierswlem  46274  fouriersw  46275  etransclem44  46322  sge0split  46453  islininds2  48522  digexp  48645