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  2208  grpoidinvlem3  20873  atomli  22962  arg-ax  24855  mapmapmap  25148  domrancur1c  25202  mslb1  25607  iintlem1  25610  pgapspf2  26053  prter1  26747  ioovolcl  27742  abnotataxb  27885  abcdtb  27891  abcdtc  27892  abcdtd  27893  3vfriswmgra  28183  1to2vfriswmgra  28184
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