Theorem syl6 33

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)

Hypotheses

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

Assertion

Ref	Expression
syl6	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6

Step	Hyp	Ref	Expression
1		syl6.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl6.2	. . 3 |- ( ch -> th )
3	2	a1i 9	. 2 |- ( ps -> ( ch -> th ) )
4	1, 3	sylcom 28	1 |- ( ph -> ( ps -> 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:  syl56  34  syl6com  35  a1dd  48  syl6mpi  64  syl6c  66  com34  83  ex  115  imbitrdi  161  imbitrrdi  162  biimtrdi  163  biimtrrdi  164  pm5.32d  450  con2d  627  con3d  634  expi  641  pm3.37  693  pm5.21ndd  710  pm2.37  810  pm2.81  816  dcim  846  condcOLD  859  con4biddc  862  pm2.54dc  896  pm4.79dc  908  pm2.85dc  910  pm3.12dc  964  dn1dc  966  3jao  1335  xoranor  1419  syl6an  1476  syl10  1477  hbald  1537  ax12  1558  hbimd  1619  nfal  1622  19.21ht  1627  19.30dc  1673  19.23t  1723  hbexd  1740  spimth  1781  spimed  1786  cbv2h  1794  cbv2w  1796  equvini  1804  sbiedh  1833  sbcof2  1856  aev  1858  sb3  1877  hbsb2  1882  sbequilem  1884  sbft  1894  sbi1v  1938  cbvexdh  1973  nf5-1  2075  mo23  2119  moexexdc  2162  euexex  2163  exists2  2175  dvelimdc  2393  rsp2  2580  rgen2a  2584  spcimgft  2879  spcimegft  2881  eueq3dc  2977  moeq3dc  2979  reu6  2992  ssddif  3438  reupick2  3490  ifnebibdc  3648  sssnm  3832  prneimg  3852  dfiun2g  3997  exmidsssnc  4287  exmidundifim  4291  opth1  4322  copsexg  4330  opelopabt  4350  issod  4410  sowlin  4411  suctr  4512  reusv3i  4550  ralxfrALT  4558  ssorduni  4579  onintonm  4609  regexmidlem1  4625  nlimsucg  4658  0elnn  4711  ssrelrn  4914  issref  5111  iotaval  5290  fun11iun  5595  brprcneu  5622  fvssunirng  5644  relfvssunirn  5645  fv3  5652  ndmfvg  5660  ssimaex  5697  fvopab3ig  5710  dff4im  5783  ffnfv  5795  fconstfvm  5861  f1mpt  5901  oprabid  6039  mpoeq123  6069  f1o2ndf1  6380  brtposg  6406  rntpos  6409  dftpos4  6415  smores2  6446  tfri3  6519  rdgss  6535  nntri3or  6647  nndifsnid  6661  nnawordex  6683  eroveu  6781  map0g  6843  fundmen  6967  nneneq  7026  fiintim  7104  snon0  7113  fnfi  7114  infnlbti  7204  exmidonfinlem  7382  exmidontri2or  7439  addclpi  7525  enq0tr  7632  genprndl  7719  genprndu  7720  genpdisj  7721  addlocprlem  7733  nqprloc  7743  recexprlemss1l  7833  recexprlemss1u  7834  suplocexprlemss  7913  elrealeu  8027  ltleletr  8239  negf1o  8539  zletric  9501  zlelttric  9502  zltnle  9503  zmulcl  9511  zdcle  9534  zdclt  9535  zeo  9563  uz11  9757  indstr  9800  eqreznegel  9821  negm  9822  lbzbi  9823  fzdcel  10248  fzm1  10308  qletric  10473  qlelttric  10474  qltnle  10475  qdclt  10477  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  qsqeqor  10884  swrdccatin2d  11291  rennim  11528  maxleast  11739  negfi  11754  fsum3cvg  11904  fproddccvg  12098  prodmodc  12104  ndvdssub  12456  bitsinv1lem  12487  algcvgblem  12586  algcvga  12588  isprm3  12655  oddprmdvds  12892  4sqlem2  12927  imasaddfnlemg  13362  subrngintm  14191  subrgintm  14222  lmodfopnelem1  14303  islssm  14336  lspsneq0  14405  islidlm  14458  epttop  14779  cnptoprest  14928  txcnp  14960  metequiv2  15185  cnlimcim  15360  umgrclwwlkge2  16139  bj-hbalt  16182  bj-intabssel1  16209  decidin  16216  sumdc2  16218  bj-charfunr  16228  bj-axemptylem  16310  bj-nnen2lp  16372  bj-nnord  16376  setindft  16383  bj-inf2vnlem2  16389  bj-inf2vnlem3  16390  bj-inf2vnlem4  16391  exmidsbthrlem  16450  triap  16457  tridceq  16484