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  speimfw  1722  axc11nlem  1924  axc11nlemOLD  2034  axc11n  2035  axc11nOLD  2036  axc16i  2050  mo2vOLD  2276  mo2vOLDOLD  2277  eupickbi  2347  2moOLD  2360  ceqsalgALT  3121  cgsexg  3128  cgsex2g  3129  cgsex4g  3130  spc2egv  3182  spc3egv  3184  disjne  3858  uneqdifeq  3902  triun  4543  sucssel  4960  relresfld  5524  relcoi1  5526  unixpid  5532  fvimacnv  5987  ordsuc  6634  tfi  6673  fornex  6754  f1ovv  6756  tz7.49  7112  oeworde  7244  undifixp  7507  dom2d  7558  findcard  7761  fisupg  7770  dffi3  7893  noinfep  8079  cantnflem2  8112  tcmin  8175  rankr1ag  8223  rankpwi  8244  rankelb  8245  rankunb  8271  rankxpsuc  8303  alephordi  8458  alephsucdom  8463  alephinit  8479  dfac9  8519  ackbij2lem4  8625  cff1  8641  cfslbn  8650  cfcoflem  8655  cfcof  8657  infpssrlem5  8690  isfin7-2  8779  acncc  8823  domtriomlem  8825  axdc3lem2  8834  ttukeylem1  8892  iundom2g  8918  axpowndlem3  8978  wunex2  9119  grupr  9178  gruiun  9180  eltskm  9224  nqereu  9310  addcanpr  9427  axpre-sup  9549  relin01  10084  nneo  10953  zeo2  10956  xrub  11514  uznfz  11772  difelfzle  11799  ssfzo12  11887  facndiv  12348  hashf1rn  12407  hashgt12el2  12464  hash2prde  12498  hash2prd  12500  hash2pwpr  12501  exprelprel  12510  brfi1uzind  12514  swrdswrd  12667  swrdccatin2  12694  swrdccatin12lem2  12696  swrdccatin12  12698  swrdccat3  12699  swrdccatid  12704  repswswrd  12738  2cshwcshw  12775  fsumcom2  13571  incexclem  13630  fprodss  13737  fprodcom2  13770  ndvdssub  14047  eucalglt  14196  prmind2  14210  coprm  14223  prmdiveq  14298  drsdir  15543  lublecllem  15597  istos  15644  tsrlin  15828  dirge  15846  mhmlin  15952  issubg2  16195  nsgbi  16211  symgextf1lem  16424  sylow2a  16618  issubrg2  17428  abvmul  17457  abvtri  17458  lmodlema  17496  lspsnel6  17619  lmhmlin  17660  lbsind  17705  0ring01eq  17898  01eq0ring  17899  gsummoncoe1  18325  cygth  18588  ipcj  18647  obsip  18730  lindsss  18837  mamufacex  18869  mavmulsolcl  19031  slesolvec  19159  inopn  19386  basis1  19429  tgss  19448  tgcl  19449  elcls3  19562  neindisj2  19602  cnpco  19746  cncls  19753  1stcelcls  19940  txkgen  20131  qtoptop2  20178  nrmr0reg  20228  fbasssin  20315  fbfinnfr  20320  fbunfip  20348  filufint  20399  uffix  20400  ufinffr  20408  ufilen  20409  fmfnfmlem1  20433  flftg  20475  alexsubALT  20529  xmeteq0  20819  blssexps  20907  blssex  20908  mopni3  20975  neibl  20982  metss  20989  metcnp3  21021  nmvs  21163  reperflem  21301  iccntr  21304  reconnlem2  21310  lebnumlem3  21441  caubl  21724  bcthlem5  21745  ovolunlem1  21886  voliunlem1  21938  volsuplem  21943  ellimc3  22261  lhop1lem  22392  ulmss  22770  dchrisumlema  23651  usgrarnedg  24362  usgrafisbase  24392  sizeusglecusglem1  24462  uvtxisvtx  24468  wlkn0  24505  usgrnloop  24543  usgra2wlkspthlem1  24597  usgrcyclnl2  24619  wlk0  24739  clwwlknprop  24750  clwlkisclwwlklem0  24766  wwlkext2clwwlk  24781  clwlkfclwwlk  24822  usgfiregdegfi  24889  eupatrl  24946  2pthfrgra  24989  3cyclfrgrarn2  24992  frgrancvvdeqlemB  25016  frgrawopreg1  25028  frgrawopreg2  25029  frgraeu  25032  numclwwlkovf2ex  25064  frgraregord013  25096  frgraogt3nreg  25098  ablocom  25265  rngodm1dm2  25398  rngoueqz  25410  zerdivemp1  25414  rngoridfz  25415  ubthlem1  25764  shaddcl  26112  shmulcl  26113  shmulclOLD  26114  spansnss2  26471  cnopc  26810  cnfnc  26827  adj1  26830  pjorthcoi  27066  stj  27132  mdsl1i  27218  chirredlem1  27287  mdsymlem5  27304  cdj3lem2b  27334  slmdlema  27724  pconcn  28647  cvmlift2lem1  28725  ss2mcls  28906  dfon2lem6  29196  wfrlem4  29322  wfrlem10  29328  frrlem4  29366  nofv  29393  nodenselem4  29420  waj-ax  29855  lukshef-ax2  29856  ontgval  29872  nn0prpw  30117  heiborlem1  30283  zerdivemp1x  30334  isdrngo3  30338  0rngo  30400  pridl  30410  ispridlc  30443  isdmn3  30447  dmnnzd  30448  dfac21  30988  2f1fvneq  32261  imarnf1pr  32263  2ffzoeq  32295  usgrauvtxvd  32312  usgo0s0  32389  usgo0s0ALT  32390  usgo1s0ALT  32391  usgo1s0  32396  usgresvm1  32397  usgresvm1ALT  32401  gsumpr  32818  lincdifsn  32895  snlindsntor  32942  lincresunit3lem1  32950  lincresunit3lem2  32951  lincresunit3  32952  eexinst11  33165  ax6e2eq  33198  e222  33290  e111  33328  eel12131  33374  e333  33398  bj-alrim  34129  bj-nexdt  34133  bj-axc11nlemv  34198  bj-axc11nv  34199  lshpcmp  34588  omllaw  34843  dochexmidlem7  37068  lspindp5  37372