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  2880  spcimegft  2882  eueq3dc  2978  moeq3dc  2980  reu6  2993  ssddif  3439  reupick2  3491  ifnebibdc  3649  sssnm  3835  prneimg  3855  dfiun2g  4000  exmidsssnc  4291  exmidundifim  4295  opth1  4326  copsexg  4334  opelopabt  4354  issod  4414  sowlin  4415  suctr  4516  reusv3i  4554  ralxfrALT  4562  ssorduni  4583  onintonm  4613  regexmidlem1  4629  nlimsucg  4662  0elnn  4715  ssrelrn  4920  issref  5117  iotaval  5296  fun11iun  5601  brprcneu  5628  fvssunirng  5650  relfvssunirn  5651  fv3  5658  ndmfvg  5666  ssimaex  5703  fvopab3ig  5716  dff4im  5789  ffnfv  5801  fconstfvm  5867  f1mpt  5907  oprabid  6045  mpoeq123  6075  f1o2ndf1  6388  brtposg  6415  rntpos  6418  dftpos4  6424  smores2  6455  tfri3  6528  rdgss  6544  nntri3or  6656  nndifsnid  6670  nnawordex  6692  eroveu  6790  map0g  6852  fundmen  6976  nneneq  7038  fiintim  7116  snon0  7125  fnfi  7126  infnlbti  7216  exmidonfinlem  7394  exmidontri2or  7451  addclpi  7537  enq0tr  7644  genprndl  7731  genprndu  7732  genpdisj  7733  addlocprlem  7745  nqprloc  7755  recexprlemss1l  7845  recexprlemss1u  7846  suplocexprlemss  7925  elrealeu  8039  ltleletr  8251  negf1o  8551  zletric  9513  zlelttric  9514  zltnle  9515  zmulcl  9523  zdcle  9546  zdclt  9547  zeo  9575  uz11  9769  indstr  9817  eqreznegel  9838  negm  9839  lbzbi  9840  fzdcel  10265  fzm1  10325  qletric  10491  qlelttric  10492  qltnle  10493  qdclt  10495  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  qsqeqor  10902  swrdccatin2d  11315  rennim  11553  maxleast  11764  negfi  11779  fsum3cvg  11929  fproddccvg  12123  prodmodc  12129  ndvdssub  12481  bitsinv1lem  12512  algcvgblem  12611  algcvga  12613  isprm3  12680  oddprmdvds  12917  4sqlem2  12952  imasaddfnlemg  13387  subrngintm  14216  subrgintm  14247  lmodfopnelem1  14328  islssm  14361  lspsneq0  14430  islidlm  14483  epttop  14804  cnptoprest  14953  txcnp  14985  metequiv2  15210  cnlimcim  15385  umgrclwwlkge2  16197  bj-hbalt  16295  bj-intabssel1  16322  decidin  16329  sumdc2  16331  bj-charfunr  16341  bj-axemptylem  16423  bj-nnen2lp  16485  bj-nnord  16489  setindft  16496  bj-inf2vnlem2  16502  bj-inf2vnlem3  16503  bj-inf2vnlem4  16504  exmidsbthrlem  16562  triap  16569  tridceq  16596