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

Theorem syl6com 35
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypotheses
Ref Expression
syl6com.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6com.2  |-  ( ch 
->  th )
Assertion
Ref Expression
syl6com  |-  ( ps 
->  ( ph  ->  th )
)

Proof of Theorem syl6com
StepHypRef Expression
1 syl6com.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6com.2 . . 3  |-  ( ch 
->  th )
31, 2syl6 33 . 2  |-  ( ph  ->  ( ps  ->  th )
)
43com12 31 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  19.33b  1663  ax6e  1946  axc16i  2012  wefrc  4726  elres  5157  sorpssuni  6381  sorpssint  6382  ordzsl  6468  limuni3  6475  funcnvuni  6542  funrnex  6556  soxp  6697  oaabs  7095  eceqoveq  7217  php3  7509  pssinf  7535  unbnn2  7581  inf0  7839  inf3lem5  7850  tcel  7977  rankxpsuc  8101  carduni  8163  prdom2  8185  dfac5  8310  cflm  8431  indpi  9088  prlem934  9214  xrub  11286  injresinjlem  11650  hashgt12el  12185  hashgt12el2  12186  brfi1uzind  12231  cshwshash  14143  symgextf1  15938  basis2  18568  bwthOLD  19026  fbdmn0  19419  usgranloopv  23309  nbgranself2  23359  usgrnloop  23474  wlkdvspthlem  23518  rngoueqz  23929  atcv0eq  25795  dfon2lem9  27616  trpredrec  27714  frmin  27715  wfrlem4  27739  wfrlem12  27747  frrlem4  27783  frrlem11  27792  altopthsn  28004  rankeq1o  28221  wl-equsb4  28393  hbtlem5  29496  funressnfv  30046  afvco2  30094  ndmaovcl  30121  erclwwlktr0  30491  4cyclusnfrgra  30623  frgrancvvdeqlem7  30641  frgrawopreglem2  30650  gsummoncoe1  30855  zlmodzxznm  31051
  Copyright terms: Public domain W3C validator