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  2888  prneimg  4361  ordtri3OLD  5722  ssxr  10052  isirred2  18617  aaliou3lem9  24004  mideulem2  25521  opphllem  25522  bj-dfbi4  32192  topdifinffinlem  32819  icorempt2  32823  dalawlem13  34635  cdleme22b  35095  jm2.26lem3  37034  wopprc  37063  iunconnlem2  38640  icccncfext  39391  cncfiooicc  39398  fourierdlem25  39643  fourierdlem35  39653  fourierswlem  39741  fouriersw  39742  etransclem44  39789  sge0split  39920  islininds2  41535  digexp  41667