Theorem pm4.56 986

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   ∨ wo 844

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 397  df-or 845

This theorem is referenced by:  oran  987  neanior  3037  rexprg  4632  prneimg  4785  ord1eln01  8326  ord2eln012  8327  unfi  8955  ssxr  11044  isirred2  19943  aaliou3lem9  25510  mideulem2  27095  opphllem  27096  bj-dfbi4  34754  topdifinffinlem  35518  icorempo  35522  dalawlem13  37897  cdleme22b  38355  metakunt1  40125  negn0nposznnd  40310  jm2.26lem3  40823  wopprc  40852  iunconnlem2  42555  icccncfext  43428  cncfiooicc  43435  fourierdlem25  43673  fourierdlem35  43683  fourierswlem  43771  fouriersw  43772  etransclem44  43819  sge0split  43947  islininds2  45825  digexp  45953