Theorem pm4.56 1012

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

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 385   ∨ wo 874

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 199  df-an 386  df-or 875

This theorem is referenced by:  oran  1013  neanior  3061  prneimg  4571  ssxr  10395  isirred2  19014  aaliou3lem9  24443  mideulem2  25975  opphllem  25976  bj-dfbi4  33054  topdifinffinlem  33685  icorempt2  33689  dalawlem13  35896  cdleme22b  36354  jm2.26lem3  38341  wopprc  38370  iunconnlem2  39919  icccncfext  40832  cncfiooicc  40839  fourierdlem25  41080  fourierdlem35  41090  fourierswlem  41178  fouriersw  41179  etransclem44  41226  sge0split  41357  islininds2  43060  digexp  43188