Theorem pm4.56 987

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395   ∨ wo 846

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 206  df-an 396  df-or 847

This theorem is referenced by:  oran  988  neanior  3032  rexprg  4701  prneimg  4856  ord1eln01  8516  ord2eln012  8517  unfi  9196  ssxr  11313  isirred2  20359  aaliou3lem9  26284  mideulem2  28537  opphllem  28538  bj-dfbi4  36049  topdifinffinlem  36826  icorempo  36830  dalawlem13  39356  cdleme22b  39814  aks6d1c2p2  41590  metakunt1  41657  negn0nposznnd  41856  jm2.26lem3  42422  wopprc  42451  iunconnlem2  44374  icccncfext  45275  cncfiooicc  45282  fourierdlem25  45520  fourierdlem35  45530  fourierswlem  45618  fouriersw  45619  etransclem44  45666  sge0split  45797  islininds2  47552  digexp  47680