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  3022  rexprg  4651  prneimg  4807  ord1eln01  8419  ord2eln012  8420  unfi  9089  ssxr  11191  isirred2  20343  aaliou3lem9  26288  mideulem2  28715  opphllem  28716  weiunfr  36534  bj-dfbi4  36640  topdifinffinlem  37414  icorempo  37418  dalawlem13  40005  cdleme22b  40463  aks6d1c2p2  42235  negn0nposznnd  42403  jm2.26lem3  43121  wopprc  43150  iunconnlem2  45054  icccncfext  46012  cncfiooicc  46019  fourierdlem25  46257  fourierdlem35  46267  fourierswlem  46355  fouriersw  46356  etransclem44  46403  sge0split  46534  islininds2  48612  digexp  48735