Theorem pm4.56 986

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 844

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 210  df-an 400  df-or 845

This theorem is referenced by:  oran  987  nornotOLD  1526  neanior  3079  prneimg  4745  ssxr  10699  isirred2  19447  aaliou3lem9  24946  mideulem2  26528  opphllem  26529  bj-dfbi4  34019  topdifinffinlem  34764  icorempo  34768  dalawlem13  37179  cdleme22b  37637  metakunt1  39350  negn0nposznnd  39476  jm2.26lem3  39942  wopprc  39971  iunconnlem2  41641  icccncfext  42529  cncfiooicc  42536  fourierdlem25  42774  fourierdlem35  42784  fourierswlem  42872  fouriersw  42873  etransclem44  42920  sge0split  43048  islininds2  44893  digexp  45021