Theorem pm4.56 515

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

Syntax hints:  ¬ wn 3   ↔ wb 195   ∨ 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 196  df-or 384  df-an 385

This theorem is referenced by:  oran  516  neanior  2874  prneimg  4328  ordtri3OLD  5677  ssxr  9986  isirred2  18524  aaliou3lem9  23909  mideulem2  25426  opphllem  25427  bj-dfbi4  31728  topdifinffinlem  32371  icorempt2  32375  dalawlem13  34187  cdleme22b  34647  jm2.26lem3  36586  wopprc  36615  iunconlem2  38193  icccncfext  38773  cncfiooicc  38780  fourierdlem25  39025  fourierdlem35  39035  fourierswlem  39123  fouriersw  39124  etransclem44  39171  sge0split  39302  islininds2  42067  digexp  42199