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  3034  rexprg  4696  prneimg  4853  ord1eln01  8535  ord2eln012  8536  unfi  9212  ssxr  11331  isirred2  20422  aaliou3lem9  26393  mideulem2  28743  opphllem  28744  weiunfr  36469  bj-dfbi4  36575  topdifinffinlem  37349  icorempo  37353  dalawlem13  39886  cdleme22b  40344  aks6d1c2p2  42121  metakunt1  42207  negn0nposznnd  42322  jm2.26lem3  43018  wopprc  43047  iunconnlem2  44960  icccncfext  45907  cncfiooicc  45914  fourierdlem25  46152  fourierdlem35  46162  fourierswlem  46250  fouriersw  46251  etransclem44  46298  sge0split  46429  islininds2  48406  digexp  48533