Theorem pm4.56 996

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

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  oran  997  neanior  3028  rexprg  4636  prneimg  4792  ord1eln01  8428  ord2eln012  8429  unfi  9102  ssxr  11213  isirred2  20399  aaliou3lem9  26341  mideulem2  28827  opphllem  28828  weiunfr  36702  bj-dfbi4  36891  topdifinffinlem  37716  icorempo  37720  dalawlem13  40382  cdleme22b  40840  aks6d1c2p2  42611  negn0nposznnd  42766  jm2.26lem3  43453  wopprc  43482  iunconnlem2  45385  icccncfext  46337  cncfiooicc  46344  fourierdlem25  46582  fourierdlem35  46592  fourierswlem  46680  fouriersw  46681  etransclem44  46728  sge0split  46859  islininds2  48982  digexp  49105