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

Theorem pm4.56 495
Description: Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm4.56  |-  ( ( -.  ph  /\  -.  ps ) 
<->  -.  ( ph  \/  ps ) )

Proof of Theorem pm4.56
StepHypRef Expression
1 ioran 490 . 2  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )
21bicomi 202 1  |-  ( ( -.  ph  /\  -.  ps ) 
<->  -.  ( ph  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    \/ wo 368    /\ wa 369
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 185  df-or 370  df-an 371
This theorem is referenced by:  oran  496  neanior  2792  prneimg  4207  ordtri3  4914  ssxr  9650  isirred2  17131  aaliou3lem9  22477  coltr2  23738  mideulem  23810  jm2.26lem3  30547  wopprc  30576  icccncfext  31226  cncfiooicc  31233  fourierdlem25  31432  fourierdlem35  31442  fourierswlem  31531  islininds2  32158  iunconlem2  32815  bj-dfbi4  33221  dalawlem13  34679  cdleme22b  35137
  Copyright terms: Public domain W3C validator