Theorem pm4.56 517

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

Syntax hints:  ¬ wn 3   ↔ wb 196   ∨ wo 382   ∧ wa 383

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 197  df-or 384  df-an 385

This theorem is referenced by:  oran  518  neanior  3016  prneimg  4524  ordtri3OLD  5913  ssxr  10291  isirred2  18893  aaliou3lem9  24296  mideulem2  25817  opphllem  25818  bj-dfbi4  32856  topdifinffinlem  33498  icorempt2  33502  dalawlem13  35664  cdleme22b  36123  jm2.26lem3  38062  wopprc  38091  iunconnlem2  39662  icccncfext  40595  cncfiooicc  40602  fourierdlem25  40844  fourierdlem35  40854  fourierswlem  40942  fouriersw  40943  etransclem44  40990  sge0split  41121  islininds2  42775  digexp  42903