MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.56 Structured version   Visualization version   GIF version

Theorem pm4.56 988
Description: Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm4.56 ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))

Proof of Theorem pm4.56
StepHypRef Expression
1 ioran 983 . 2 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
21bicomi 223 1 ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397  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 398  df-or 847
This theorem is referenced by:  oran  989  neanior  3038  rexprg  4662  prneimg  4817  ord1eln01  8447  ord2eln012  8448  unfi  9123  ssxr  11231  isirred2  20139  aaliou3lem9  25726  mideulem2  27718  opphllem  27719  bj-dfbi4  35066  topdifinffinlem  35847  icorempo  35851  dalawlem13  38375  cdleme22b  38833  aks6d1c2p2  40578  metakunt1  40606  negn0nposznnd  40825  jm2.26lem3  41354  wopprc  41383  iunconnlem2  43291  icccncfext  44202  cncfiooicc  44209  fourierdlem25  44447  fourierdlem35  44457  fourierswlem  44545  fouriersw  44546  etransclem44  44593  sge0split  44724  islininds2  46639  digexp  46767
  Copyright terms: Public domain W3C validator