Theorem pm4.56 1004

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  oran  1005  neanior  3057  rexprg  4665  prneimg  4820  ord1eln01  8477  ord2eln012  8478  unfi  9151  ssxr  11275  isirred2  20499  aaliou3lem9  26476  mideulem2  28970  opphllem  28971  weiunfr  36863  bj-dfbi4  37051  topdifinffinlem  37876  icorempo  37880  dalawlem13  40542  cdleme22b  41000  aks6d1c2p2  42771  negn0nposznnd  42926  jm2.26lem3  43613  wopprc  43642  iunconnlem2  45528  icccncfext  46486  cncfiooicc  46493  fourierdlem25  46731  fourierdlem35  46741  fourierswlem  46829  fouriersw  46830  etransclem44  46877  sge0split  47008  islininds2  49142  digexp  49265