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

Theorem pm3.22 450
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 449 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
21imp 430 1  |-  ( (
ph  /\  ps )  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ancom  451  ancom2s  809  ancom1s  812  brfi1uzind  12647  cshwlen  12892  prmgapprmorlemOLD  15005  prmgapprmolem  15020  mat1dimcrng  19489  dmatcrng  19514  cramerlem1  19699  cramer  19703  pmatcollpwscmatlem2  19801  constr3lem4  25361  constr3trllem2  25365  constr3trllem3  25366  clwwlkprop  25484  3vfriswmgra  25719  1to2vfriswmgra  25720  frg2woteq  25774  numclwwlkovfel2  25797  frgrareggt1  25830  grpoidinvlem3  25920  atomli  28021  arg-ax  31069  cnambfre  31903  prter1  32369  dvdsn1add  37634  fourierdlem42  37832  fourierdlem42OLD  37833  fourierdlem80  37870  etransclem38  37957  gbegt5  38574  c0snmhm  39187  pgrpgt2nabl  39425
  Copyright terms: Public domain W3C validator