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  1683  ax6e  1988  axc16i  2050  rgen2a  2870  wefrc  4863  elres  5299  sorpssuni  6574  sorpssint  6575  ordzsl  6665  limuni3  6672  funcnvuni  6738  funrnex  6752  soxp  6898  oaabs  7295  eceqoveq  7418  php3  7705  pssinf  7732  unbnn2  7779  inf0  8041  inf3lem5  8052  tcel  8179  rankxpsuc  8303  carduni  8365  prdom2  8387  dfac5  8512  cflm  8633  indpi  9288  prlem934  9414  xrub  11512  injresinjlem  11904  hashgt12el  12460  hashgt12el2  12461  brfi1uzind  12511  cshwcsh2id  12775  cshwshash  14466  symgextf1  16320  gsummoncoe1  18220  basis2  19325  bwthOLD  19784  fbdmn0  20208  usgranloopv  24250  nbgranself2  24308  usgrnloop  24437  wlkdvspthlem  24481  4cyclusnfrgra  24891  frgrancvvdeqlem7  24908  rngoueqz  25304  atcv0eq  27170  dfon2lem9  29198  trpredrec  29296  frmin  29297  wfrlem4  29321  wfrlem12  29329  frrlem4  29365  frrlem11  29374  altopthsn  29586  rankeq1o  29803  wl-equsb4  29980  hbtlem5  31052  funressnfv  32051  afvco2  32099  ndmaovcl  32126  zlmodzxznm  32833
  Copyright terms: Public domain W3C validator