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  3024  prneimg  4532  ordtri3OLD  5921  ssxr  10319  isirred2  18921  aaliou3lem9  24324  mideulem2  25846  opphllem  25847  bj-dfbi4  32886  topdifinffinlem  33524  icorempt2  33528  dalawlem13  35690  cdleme22b  36149  jm2.26lem3  38088  wopprc  38117  iunconnlem2  39688  icccncfext  40621  cncfiooicc  40628  fourierdlem25  40870  fourierdlem35  40880  fourierswlem  40968  fouriersw  40969  etransclem44  41016  sge0split  41147  islininds2  42801  digexp  42929