MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.22 Unicode version

Theorem pm3.22 436
Description: Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
pm3.22  |-  ( (
ph  /\  ps )  ->  ( ps  /\  ph ) )

Proof of Theorem pm3.22
StepHypRef Expression
1 pm3.21 435 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
21imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ps  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ancom  437  ancom2s  777  ancom1s  780  eupickb  2221  grpoidinvlem3  20889  atomli  22978  arg-ax  24927  mapmapmap  25251  domrancur1c  25305  mslb1  25710  iintlem1  25713  pgapspf2  26156  prter1  26850  ioovolcl  27845  abnotataxb  27988  abcdtb  27994  abcdtc  27995  abcdtd  27996  constr3lem4  28393  constr3trllem2  28397  constr3trllem3  28398  3vfriswmgra  28429  1to2vfriswmgra  28430
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator