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  1804  axc11nlem  2032  axc11nlemALT  2153  axc11n  2154  axc11nALT  2155  axc16i  2167  eupickbi  2379  ceqsalgALT  3085  cgsexg  3092  cgsex2g  3093  cgsex4g  3094  spc2egv  3148  spc3egv  3150  disjne  3822  uneqdifeq  3868  triun  4524  relresfld  5381  relcoi1OLD  5384  unixpid  5390  sucssel  5534  fvimacnv  6020  ordsuc  6668  tfi  6707  fornex  6789  f1ovv  6791  wfrlem4  7065  wfrlem10  7071  tz7.49  7188  oeworde  7320  undifixp  7584  dom2d  7636  findcard  7836  fisupg  7845  dffi3  7971  fiinfg  8041  noinfep  8191  cantnflem2  8221  tcmin  8251  rankr1ag  8299  rankpwi  8320  rankelb  8321  rankunb  8347  rankxpsuc  8379  alephordi  8531  alephsucdom  8536  alephinit  8552  dfac9  8592  ackbij2lem4  8698  cff1  8714  cfslbn  8723  cfcoflem  8728  cfcof  8730  infpssrlem5  8763  isfin7-2  8852  acncc  8896  domtriomlem  8898  axdc3lem2  8907  ttukeylem1  8965  iundom2g  8991  axpowndlem3  9050  wunex2  9189  grupr  9248  gruiun  9250  eltskm  9294  nqereu  9380  addcanpr  9497  axpre-sup  9619  relin01  10166  nneo  11048  zeo2  11051  xrub  11626  uznfz  11906  difelfzle  11934  ssfzo12  12035  facndiv  12505  hashf1rn  12567  hashgt12el2  12629  hash2prde  12664  hash2pwpr  12668  fi1uzind  12683  swrdswrd  12853  swrdccatin2  12880  swrdccatin12lem2  12882  swrdccatin12  12884  swrdccat3  12885  swrdccatid  12890  repswswrd  12924  2cshwcshw  12961  relexpcnvd  13148  relexpdmd  13156  relexprnd  13160  relexpfldd  13162  relexpaddd  13166  fsumcom2  13884  incexclem  13943  fprodss  14051  fprodcom2  14087  ndvdssub  14437  eucalglt  14593  prmind2  14684  coprm  14706  prmdiveq  14783  prmdvdsprmop  15050  prmdvdsprmorpOLD  15065  prmgaplem5  15074  drsdir  16229  lublecllem  16283  istos  16330  tsrlin  16514  dirge  16532  mhmlin  16638  issubg2  16881  nsgbi  16897  symgextf1lem  17110  sylow2a  17320  issubrg2  18077  abvmul  18106  abvtri  18107  lmodlema  18145  lspsnel6  18266  lmhmlin  18307  lbsind  18352  0ring01eq  18544  01eq0ring  18545  gsummoncoe1  18947  cygth  19191  ipcj  19250  obsip  19333  lindsss  19431  mamufacex  19463  mavmulsolcl  19625  slesolvec  19753  inopn  19978  basis1  20014  tgss  20033  tgcl  20034  elcls3  20148  neindisj2  20188  cnpco  20332  cncls  20339  1stcelcls  20525  txkgen  20716  qtoptop2  20763  nrmr0reg  20813  fbasssin  20900  fbfinnfr  20905  fbunfip  20933  filufint  20984  uffix  20985  ufinffr  20993  ufilen  20994  fmfnfmlem1  21018  flftg  21060  alexsubALT  21115  xmeteq0  21402  blssexps  21490  blssex  21491  mopni3  21558  neibl  21565  metss  21572  metcnp3  21604  nmvs  21728  reperflem  21885  iccntr  21888  reconnlem2  21894  lebnumlem3  22040  lebnumlem3OLD  22043  caubl  22326  bcthlem5  22345  ovolunlem1  22499  voliunlem1  22552  volsuplem  22557  ellimc3  22883  lhop1lem  23014  ulmss  23401  dchrisumlema  24375  usgrarnedg  25160  usgrafisbase  25191  sizeusglecusglem1  25261  uvtxisvtx  25267  wlkn0  25304  usgrwlknloop  25342  usgra2wlkspthlem1  25396  usgrcyclnl2  25418  wlk0  25538  clwwlknprop  25549  clwlkisclwwlklem0  25565  wwlkext2clwwlk  25580  clwlkfclwwlk  25621  usgfiregdegfi  25688  eupatrl  25745  2pthfrgra  25788  3cyclfrgrarn2  25791  frgrancvvdeqlemB  25815  frgrawopreg1  25827  frgrawopreg2  25828  frgraeu  25831  numclwwlkovf2ex  25863  frgraregord013  25895  frgraogt3nreg  25897  ablocom  26062  rngodm1dm2  26195  rngoueqz  26207  zerdivemp1  26211  rngoridfz  26212  ubthlem1  26561  shaddcl  26919  shmulcl  26920  spansnss2  27277  cnopc  27615  cnfnc  27632  adj1  27635  pjorthcoi  27871  stj  27937  mdsl1i  28023  chirredlem1  28092  mdsymlem5  28109  cdj3lem2b  28139  slmdlema  28568  pconcn  29996  cvmlift2lem1  30074  ss2mcls  30255  dfon2lem6  30483  frrlem4  30566  nofv  30593  nodenselem4  30622  nn0prpw  31028  waj-ax  31123  lukshef-ax2  31124  ontgval  31140  bj-alrim  31331  bj-nexdt  31335  bj-axc11nlemv  31392  bj-axc11nv  31393  sucneqond  31813  ptrecube  31985  poimirlem26  32011  poimirlem29  32014  heiborlem1  32188  zerdivemp1x  32239  isdrngo3  32243  0rngo  32305  pridl  32315  ispridlc  32348  isdmn3  32352  dmnnzd  32353  lshpcmp  32599  omllaw  32854  dochexmidlem7  35079  lspindp5  35383  dfac21  35969  eexinst11  36928  ax6e2eq  36968  e222  37058  e111  37096  eel12131  37138  e333  37160  iccpartigtl  38775  iccpartgt  38779  bgoldbtbndlem2  38939  bgoldbtbndlem3  38940  pfxccatin12lem2  39005  pfxccatin12  39006  pfxccat3  39007  2f1fvneq  39054  imarnf1pr  39058  2ffzoeq  39106  umgrnloopv  39242  usgrnloopvALT  39332  umgrres1lem  39427  upgrres1  39430  nbuhgr  39461  cplgrop  39554  fusgrregdegfi  39636  1wlkdlem2  39726  upgrwlkdvdelem  39768  g01wlk0  39831  usgrauvtxvd  39945  usgo0s0  40020  usgo0s0ALT  40021  usgo1s0ALT  40022  usgo1s0  40027  usgresvm1  40028  usgresvm1ALT  40032  nrhmzr  40146  nzerooringczr  40347  gsumpr  40415  lincdifsn  40490  snlindsntor  40537  lincresunit3lem1  40545  lincresunit3lem2  40546  lincresunit3  40547