Theorem syl5com 30

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)

Hypotheses

Ref	Expression
syl5com.1	|- ( ph -> ps )
syl5com.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5com	|- ( ph -> ( ch -> th ) )

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 |- ( ph -> ps )
2	1	a1d 25	. 2 |- ( ph -> ( ch -> ps ) )
3		syl5com.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	sylcom 29	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com12  31  syl5  32  axc11nlem  1996  axc11n  1997  axc16i  2012  mo2vOLD  2261  mo2vOLDOLD  2262  eupickbi  2346  2moOLD  2361  ceqsalgALT  3013  cgsexg  3020  cgsex2g  3021  cgsex4g  3022  spc2egv  3074  spc3egv  3076  disjne  3739  uneqdifeq  3782  triun  4413  ordelord  4756  sucssel  4826  relresfld  5379  relcoi1  5381  unixpid  5387  fvimacnv  5833  ordsuc  6440  tfi  6479  fornex  6561  f1dmex  6562  f1ovv  6563  tz7.49  6915  oeworde  7047  undifixp  7314  dom2d  7365  2pwuninel  7481  findcard  7566  fisupg  7575  dffi3  7696  noinfep  7880  cantnflem2  7913  tcmin  7976  rankr1ag  8024  rankpwi  8045  rankelb  8046  rankunb  8072  rankxpsuc  8104  alephordi  8259  alephsucdom  8264  alephinit  8280  dfac9  8320  ackbij2lem4  8426  cff1  8442  cfslbn  8451  cfcoflem  8456  cfcof  8458  infpssrlem5  8491  isfin7-2  8580  acncc  8624  domtriomlem  8626  axdc3lem2  8635  ttukeylem1  8693  iundom2g  8719  axpowndlem3  8779  wunex2  8920  grupr  8979  gruiun  8981  eltskm  9025  nqereu  9113  addcanpr  9230  axpre-sup  9351  relin01  9879  nneo  10740  zeo2  10743  xrub  11289  uznfz  11558  ssfzo12  11635  facndiv  12079  hashf1rn  12138  hashgt12el2  12189  hash2prde  12194  hash2prd  12196  hash2pwpr  12197  brfi1uzind  12234  swrdswrd  12369  swrdccatin2  12393  swrdccatin12lem2  12395  swrdccatin12  12397  swrdccat3  12398  swrdccatid  12403  repswswrd  12437  fsumcom2  13256  incexclem  13314  isumrpcl  13321  ndvdssub  13626  eucalglt  13775  prmind2  13789  coprm  13801  prmdiveq  13876  drsdir  15120  lublecllem  15173  istos  15220  tsrlin  15404  dirge  15422  mhmlin  15486  issubg2  15711  nsgbi  15727  symgextf1lem  15940  sylow2a  16133  issubrg2  16900  abvmul  16929  abvtri  16930  lmodlema  16968  lspsnel6  17090  lmhmlin  17131  lbsind  17176  cygth  18019  ipcj  18078  obsip  18161  lindsss  18268  mamufacex  18304  mavmulsolcl  18377  slesolvec  18500  inopn  18527  basis1  18570  tgss  18588  tgcl  18589  elcls3  18702  neindisj2  18742  cnpco  18886  cncls  18893  1stcelcls  19080  txkgen  19240  qtoptop2  19287  nrmr0reg  19337  fbasssin  19424  fbfinnfr  19429  fbunfip  19457  filufint  19508  uffix  19509  ufinffr  19517  ufilen  19518  fmfnfmlem1  19542  flftg  19584  alexsubALT  19638  xmeteq0  19928  blssexps  20016  blssex  20017  mopni3  20084  neibl  20091  metss  20098  metcnp3  20130  nmvs  20272  reperflem  20410  iccntr  20413  reconnlem2  20419  lebnumlem3  20550  caubl  20833  bcthlem5  20854  ovolunlem1  20995  voliunlem1  21046  volsuplem  21051  ellimc3  21369  lhop1lem  21500  ulmss  21877  dchrisumlema  22752  usgrarnedg  23318  usgrafisbase  23342  sizeusglecusglem1  23407  uvtxisvtx  23413  usgrnloop  23477  usgrcyclnl2  23542  eupatrl  23604  ablocom  23787  rngodm1dm2  23920  rngoueqz  23932  zerdivemp1  23936  rngoridfz  23937  ubthlem1  24286  shaddcl  24634  shmulcl  24635  shmulclOLD  24636  spansnss2  24993  cnopc  25332  cnfnc  25349  adj1  25352  pjorthcoi  25588  stj  25654  mdsl1i  25740  chirredlem1  25809  mdsymlem5  25826  cdj3lem2b  25856  slmdlema  26234  pconcn  27128  cvmlift2lem1  27206  fprodss  27476  fprodcom2  27510  dfon2lem6  27616  wfrlem4  27742  wfrlem10  27748  frrlem4  27786  nofv  27813  nodenselem4  27840  waj-ax  28275  lukshef-ax2  28276  ontgval  28292  nn0prpw  28537  heiborlem1  28729  zerdivemp1x  28780  isdrngo3  28784  0rngo  28846  pridl  28856  ispridlc  28889  isdmn3  28893  dmnnzd  28894  dfac21  29438  2f1fvneq  30162  imarnf1pr  30169  2ffzoeq  30233  exprelprel  30248  wlkn0  30298  wlk0  30311  usgra2wlkspthlem1  30315  clwwlknprop  30454  clwlkisclwwlklem0  30469  wwlkext2clwwlk  30484  difelfzle  30506  cshwlemma1  30508  clwlkfclwwlk  30536  usgfiregdegfi  30547  usgrauvtxvd  30549  2pthfrgra  30622  3cyclfrgrarn2  30625  frgrancvvdeqlemB  30650  frgrawopreg1  30662  frgrawopreg2  30663  frgraeu  30666  numclwwlkovf2ex  30698  frgraregord013  30730  frgraogt3nreg  30732  gsumpr  30777  0rng01eq  30795  01eq0rng  30796  gsummoncoe1  30862  lincdifsn  30977  snlindsntor  31024  lincresunit3lem1  31032  lincresunit3lem2  31033  lincresunit3  31034  eexinst11  31251  ax6e2eq  31285  e222  31377  e111  31415  eel12131  31461  e333  31485  bj-alrim  32201  bj-nexdt  32205  bj-axc11nlemv  32269  bj-axc11nv  32270  lshpcmp  32652  omllaw  32907  dochexmidlem7  35130  lspindp5  35434