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  1707  axc11nlem  1885  axc11nlemOLD  2021  axc11n  2022  axc11nOLD  2023  axc16i  2037  mo2vOLD  2283  mo2vOLDOLD  2284  eupickbi  2368  2moOLD  2383  ceqsalgALT  3139  cgsexg  3146  cgsex2g  3147  cgsex4g  3148  spc2egv  3200  spc3egv  3202  disjne  3872  uneqdifeq  3915  triun  4553  ordelord  4900  sucssel  4970  relresfld  5532  relcoi1  5534  unixpid  5540  fvimacnv  5994  ordsuc  6627  tfi  6666  fornex  6750  f1dmex  6751  f1ovv  6752  tz7.49  7107  oeworde  7239  undifixp  7502  dom2d  7553  2pwuninel  7669  findcard  7755  fisupg  7764  dffi3  7887  noinfep  8072  cantnflem2  8105  tcmin  8168  rankr1ag  8216  rankpwi  8237  rankelb  8238  rankunb  8264  rankxpsuc  8296  alephordi  8451  alephsucdom  8456  alephinit  8472  dfac9  8512  ackbij2lem4  8618  cff1  8634  cfslbn  8643  cfcoflem  8648  cfcof  8650  infpssrlem5  8683  isfin7-2  8772  acncc  8816  domtriomlem  8818  axdc3lem2  8827  ttukeylem1  8885  iundom2g  8911  axpowndlem3  8971  wunex2  9112  grupr  9171  gruiun  9173  eltskm  9217  nqereu  9303  addcanpr  9420  axpre-sup  9542  relin01  10073  nneo  10940  zeo2  10943  xrub  11499  uznfz  11757  difelfzle  11781  ssfzo12  11869  facndiv  12330  hashf1rn  12389  hashgt12el2  12443  hash2prde  12478  hash2prd  12480  hash2pwpr  12481  exprelprel  12490  brfi1uzind  12494  swrdswrd  12644  swrdccatin2  12671  swrdccatin12lem2  12673  swrdccatin12  12675  swrdccat3  12676  swrdccatid  12681  repswswrd  12715  2cshwcshw  12752  fsumcom2  13548  incexclem  13607  isumrpcl  13614  ndvdssub  13920  eucalglt  14069  prmind2  14083  coprm  14096  prmdiveq  14171  drsdir  15418  lublecllem  15471  istos  15518  tsrlin  15702  dirge  15720  mhmlin  15784  issubg2  16011  nsgbi  16027  symgextf1lem  16240  sylow2a  16435  issubrg2  17232  abvmul  17261  abvtri  17262  lmodlema  17300  lspsnel6  17423  lmhmlin  17464  lbsind  17509  gsummoncoe1  18117  cygth  18377  ipcj  18436  obsip  18519  lindsss  18626  mamufacex  18658  mavmulsolcl  18820  slesolvec  18948  inopn  19175  basis1  19218  tgss  19236  tgcl  19237  elcls3  19350  neindisj2  19390  cnpco  19534  cncls  19541  1stcelcls  19728  txkgen  19888  qtoptop2  19935  nrmr0reg  19985  fbasssin  20072  fbfinnfr  20077  fbunfip  20105  filufint  20156  uffix  20157  ufinffr  20165  ufilen  20166  fmfnfmlem1  20190  flftg  20232  alexsubALT  20286  xmeteq0  20576  blssexps  20664  blssex  20665  mopni3  20732  neibl  20739  metss  20746  metcnp3  20778  nmvs  20920  reperflem  21058  iccntr  21061  reconnlem2  21067  lebnumlem3  21198  caubl  21481  bcthlem5  21502  ovolunlem1  21643  voliunlem1  21695  volsuplem  21700  ellimc3  22018  lhop1lem  22149  ulmss  22526  dchrisumlema  23401  usgrarnedg  24060  usgrafisbase  24090  sizeusglecusglem1  24160  uvtxisvtx  24166  wlkn0  24203  usgrnloop  24241  usgra2wlkspthlem1  24295  usgrcyclnl2  24317  wlk0  24437  clwwlknprop  24448  clwlkisclwwlklem0  24464  wwlkext2clwwlk  24479  clwlkfclwwlk  24520  usgfiregdegfi  24587  eupatrl  24644  2pthfrgra  24687  3cyclfrgrarn2  24690  frgrancvvdeqlemB  24715  frgrawopreg1  24727  frgrawopreg2  24728  frgraeu  24731  numclwwlkovf2ex  24763  frgraregord013  24795  frgraogt3nreg  24797  ablocom  24963  rngodm1dm2  25096  rngoueqz  25108  zerdivemp1  25112  rngoridfz  25113  ubthlem1  25462  shaddcl  25810  shmulcl  25811  shmulclOLD  25812  spansnss2  26169  cnopc  26508  cnfnc  26525  adj1  26528  pjorthcoi  26764  stj  26830  mdsl1i  26916  chirredlem1  26985  mdsymlem5  27002  cdj3lem2b  27032  slmdlema  27408  pconcn  28309  cvmlift2lem1  28387  fprodss  28657  fprodcom2  28691  dfon2lem6  28797  wfrlem4  28923  wfrlem10  28929  frrlem4  28967  nofv  28994  nodenselem4  29021  waj-ax  29456  lukshef-ax2  29457  ontgval  29473  nn0prpw  29718  heiborlem1  29910  zerdivemp1x  29961  isdrngo3  29965  0rngo  30027  pridl  30037  ispridlc  30070  isdmn3  30074  dmnnzd  30075  dfac21  30616  2f1fvneq  31776  imarnf1pr  31778  2ffzoeq  31810  usgrauvtxvd  31827  usgo0s0  31904  usgo0s0ALT  31905  usgo1s0ALT  31906  usgo1s0  31911  usgresvm1  31912  usgresvm1ALT  31916  mndmgm  31929  gsumpr  32014  0rng01eq  32029  01eq0rng  32030  lincdifsn  32098  snlindsntor  32145  lincresunit3lem1  32153  lincresunit3lem2  32154  lincresunit3  32155  eexinst11  32376  ax6e2eq  32410  e222  32502  e111  32540  eel12131  32586  e333  32610  bj-alrim  33328  bj-nexdt  33332  bj-axc11nlemv  33396  bj-axc11nv  33397  lshpcmp  33785  omllaw  34040  dochexmidlem7  36263  lspindp5  36567