Theorem pm4.56 989

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ 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 207  df-an 396  df-or 847

This theorem is referenced by:  oran  990  neanior  3041  rexprg  4721  prneimg  4879  ord1eln01  8552  ord2eln012  8553  unfi  9238  ssxr  11359  isirred2  20447  aaliou3lem9  26410  mideulem2  28760  opphllem  28761  weiunfr  36433  bj-dfbi4  36539  topdifinffinlem  37313  icorempo  37317  dalawlem13  39840  cdleme22b  40298  aks6d1c2p2  42076  metakunt1  42162  negn0nposznnd  42271  jm2.26lem3  42958  wopprc  42987  iunconnlem2  44906  icccncfext  45808  cncfiooicc  45815  fourierdlem25  46053  fourierdlem35  46063  fourierswlem  46151  fouriersw  46152  etransclem44  46199  sge0split  46330  islininds2  48213  digexp  48341