Theorem syl5com 31

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 26	. 2 |- ( ph -> ( ch -> ps ) )
3		syl5com.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	sylcom 30	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  32  syl5  33  speimfw  1786  axc11nlem  1998  axc11nlemOLD  2109  axc11n  2110  axc11nOLD  2111  axc16i  2125  eupickbi  2340  ceqsalgALT  3044  cgsexg  3051  cgsex2g  3052  cgsex4g  3053  spc2egv  3106  spc3egv  3108  disjne  3778  uneqdifeq  3824  triun  4469  relresfld  5319  relcoi1OLD  5322  unixpid  5328  sucssel  5472  fvimacnv  5951  ordsuc  6594  tfi  6633  fornex  6715  f1ovv  6717  wfrlem4  6989  wfrlem10  6995  tz7.49  7112  oeworde  7244  undifixp  7508  dom2d  7559  findcard  7758  fisupg  7767  dffi3  7893  fiinfg  7963  noinfep  8112  cantnflem2  8142  tcmin  8172  rankr1ag  8220  rankpwi  8241  rankelb  8242  rankunb  8268  rankxpsuc  8300  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  8970  wunex2  9109  grupr  9168  gruiun  9170  eltskm  9214  nqereu  9300  addcanpr  9417  axpre-sup  9539  relin01  10084  nneo  10965  zeo2  10968  xrub  11543  uznfz  11823  difelfzle  11850  ssfzo12  11949  facndiv  12418  hashf1rn  12480  hashgt12el2  12539  hash2prde  12574  hash2pwpr  12578  fi1uzind  12593  swrdswrd  12757  swrdccatin2  12784  swrdccatin12lem2  12786  swrdccatin12  12788  swrdccat3  12789  swrdccatid  12794  repswswrd  12828  2cshwcshw  12865  relexpcnvd  13038  relexpdmd  13046  relexprnd  13050  relexpfldd  13052  relexpaddd  13056  fsumcom2  13773  incexclem  13832  fprodss  13940  fprodcom2  13976  ndvdssub  14326  eucalglt  14482  prmind2  14573  coprm  14595  prmdiveq  14672  prmdvdsprmop  14939  prmdvdsprmorpOLD  14954  prmgaplem5  14963  drsdir  16118  lublecllem  16172  istos  16219  tsrlin  16403  dirge  16421  mhmlin  16527  issubg2  16770  nsgbi  16786  symgextf1lem  16999  sylow2a  17209  issubrg2  17966  abvmul  17995  abvtri  17996  lmodlema  18034  lspsnel6  18155  lmhmlin  18196  lbsind  18241  0ring01eq  18433  01eq0ring  18434  gsummoncoe1  18836  cygth  19079  ipcj  19138  obsip  19221  lindsss  19319  mamufacex  19351  mavmulsolcl  19513  slesolvec  19641  inopn  19866  basis1  19902  tgss  19921  tgcl  19922  elcls3  20036  neindisj2  20076  cnpco  20220  cncls  20227  1stcelcls  20413  txkgen  20604  qtoptop2  20651  nrmr0reg  20701  fbasssin  20788  fbfinnfr  20793  fbunfip  20821  filufint  20872  uffix  20873  ufinffr  20881  ufilen  20882  fmfnfmlem1  20906  flftg  20948  alexsubALT  21003  xmeteq0  21290  blssexps  21378  blssex  21379  mopni3  21446  neibl  21453  metss  21460  metcnp3  21492  nmvs  21616  reperflem  21773  iccntr  21776  reconnlem2  21782  lebnumlem3  21928  lebnumlem3OLD  21931  caubl  22214  bcthlem5  22233  ovolunlem1  22387  voliunlem1  22440  volsuplem  22445  ellimc3  22771  lhop1lem  22902  ulmss  23289  dchrisumlema  24263  usgrarnedg  25048  usgrafisbase  25079  sizeusglecusglem1  25149  uvtxisvtx  25155  wlkn0  25192  usgrwlknloop  25230  usgra2wlkspthlem1  25284  usgrcyclnl2  25306  wlk0  25426  clwwlknprop  25437  clwlkisclwwlklem0  25453  wwlkext2clwwlk  25468  clwlkfclwwlk  25509  usgfiregdegfi  25576  eupatrl  25633  2pthfrgra  25676  3cyclfrgrarn2  25679  frgrancvvdeqlemB  25703  frgrawopreg1  25715  frgrawopreg2  25716  frgraeu  25719  numclwwlkovf2ex  25751  frgraregord013  25783  frgraogt3nreg  25785  ablocom  25950  rngodm1dm2  26083  rngoueqz  26095  zerdivemp1  26099  rngoridfz  26100  ubthlem1  26449  shaddcl  26807  shmulcl  26808  spansnss2  27165  cnopc  27503  cnfnc  27520  adj1  27523  pjorthcoi  27759  stj  27825  mdsl1i  27911  chirredlem1  27980  mdsymlem5  27997  cdj3lem2b  28027  slmdlema  28465  pconcn  29894  cvmlift2lem1  29972  ss2mcls  30153  dfon2lem6  30380  frrlem4  30463  nofv  30490  nodenselem4  30517  nn0prpw  30923  waj-ax  31018  lukshef-ax2  31019  ontgval  31035  bj-alrim  31187  bj-nexdt  31191  bj-axc11nlemv  31255  bj-axc11nv  31256  sucneqond  31675  ptrecube  31847  poimirlem26  31873  poimirlem29  31876  heiborlem1  32050  zerdivemp1x  32101  isdrngo3  32105  0rngo  32167  pridl  32177  ispridlc  32210  isdmn3  32214  dmnnzd  32215  lshpcmp  32466  omllaw  32721  dochexmidlem7  34946  lspindp5  35250  dfac21  35837  eexinst11  36797  ax6e2eq  36837  e222  36929  e111  36967  eel12131  37013  e333  37036  iccpartigtl  38550  iccpartgt  38554  bgoldbtbndlem2  38714  bgoldbtbndlem3  38715  pfxccatin12lem2  38778  pfxccatin12  38779  pfxccat3  38780  2f1fvneq  38820  imarnf1pr  38822  2ffzoeq  38861  usgrnloopv  39035  umgrres1lem  39114  upgrres1  39117  nbuhgr  39147  cplgrop  39232  usgrauvtxvd  39263  usgo0s0  39338  usgo0s0ALT  39339  usgo1s0ALT  39340  usgo1s0  39345  usgresvm1  39346  usgresvm1ALT  39350  nrhmzr  39464  nzerooringczr  39665  gsumpr  39735  lincdifsn  39810  snlindsntor  39857  lincresunit3lem1  39865  lincresunit3lem2  39866  lincresunit3  39867