Theorem pm4.56 516

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

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

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 385  df-an 386

This theorem is referenced by:  oran  517  neanior  2882  prneimg  4363  ordtri3OLD  5729  ssxr  10067  isirred2  18641  aaliou3lem9  24043  mideulem2  25560  opphllem  25561  bj-dfbi4  32253  topdifinffinlem  32866  icorempt2  32870  dalawlem13  34688  cdleme22b  35148  jm2.26lem3  37087  wopprc  37116  iunconnlem2  38693  icccncfext  39435  cncfiooicc  39442  fourierdlem25  39686  fourierdlem35  39696  fourierswlem  39784  fouriersw  39785  etransclem44  39832  sge0split  39963  islininds2  41591  digexp  41723