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  625  con3d  632  expi  639  pm3.37  691  pm5.21ndd  707  pm2.37  807  pm2.81  813  dcim  843  condcOLD  856  con4biddc  859  pm2.54dc  893  pm4.79dc  905  pm2.85dc  907  pm3.12dc  961  dn1dc  963  3jao  1314  xoranor  1397  syl6an  1454  syl10  1455  hbald  1515  ax12  1536  hbimd  1597  nfal  1600  19.21ht  1605  19.30dc  1651  19.23t  1701  hbexd  1718  spimth  1759  spimed  1764  cbv2h  1772  cbv2w  1774  equvini  1782  sbiedh  1811  sbcof2  1834  aev  1836  sb3  1855  hbsb2  1860  sbequilem  1862  sbft  1872  sbi1v  1916  cbvexdh  1951  nf5-1  2053  mo23  2096  moexexdc  2139  euexex  2140  exists2  2152  dvelimdc  2370  rsp2  2557  rgen2a  2561  spcimgft  2853  spcimegft  2855  eueq3dc  2951  moeq3dc  2953  reu6  2966  ssddif  3411  reupick2  3463  ifnebibdc  3619  sssnm  3800  prneimg  3820  dfiun2g  3964  exmidsssnc  4254  exmidundifim  4258  opth1  4287  copsexg  4295  opelopabt  4315  issod  4373  sowlin  4374  suctr  4475  reusv3i  4513  ralxfrALT  4521  ssorduni  4542  onintonm  4572  regexmidlem1  4588  nlimsucg  4621  0elnn  4674  ssrelrn  4877  issref  5073  iotaval  5251  fun11iun  5554  brprcneu  5581  fvssunirng  5603  relfvssunirn  5604  fv3  5611  ndmfvg  5619  ssimaex  5652  fvopab3ig  5665  dff4im  5738  ffnfv  5750  fconstfvm  5814  f1mpt  5852  oprabid  5988  mpoeq123  6016  f1o2ndf1  6326  brtposg  6352  rntpos  6355  dftpos4  6361  smores2  6392  tfri3  6465  rdgss  6481  nntri3or  6591  nndifsnid  6605  nnawordex  6627  eroveu  6725  map0g  6787  fundmen  6911  nneneq  6968  fiintim  7042  snon0  7051  fnfi  7052  infnlbti  7142  exmidonfinlem  7316  exmidontri2or  7370  addclpi  7455  enq0tr  7562  genprndl  7649  genprndu  7650  genpdisj  7651  addlocprlem  7663  nqprloc  7673  recexprlemss1l  7763  recexprlemss1u  7764  suplocexprlemss  7843  elrealeu  7957  ltleletr  8169  negf1o  8469  zletric  9431  zlelttric  9432  zltnle  9433  zmulcl  9441  zdcle  9464  zdclt  9465  zeo  9493  uz11  9686  indstr  9729  eqreznegel  9750  negm  9751  lbzbi  9752  fzdcel  10177  fzm1  10237  qletric  10401  qlelttric  10402  qltnle  10403  qdclt  10405  frecuzrdgtcl  10574  frecuzrdgfunlem  10581  qsqeqor  10812  rennim  11383  maxleast  11594  negfi  11609  fsum3cvg  11759  fproddccvg  11953  prodmodc  11959  ndvdssub  12311  bitsinv1lem  12342  algcvgblem  12441  algcvga  12443  isprm3  12510  oddprmdvds  12747  4sqlem2  12782  imasaddfnlemg  13216  subrngintm  14044  subrgintm  14075  lmodfopnelem1  14156  islssm  14189  lspsneq0  14258  islidlm  14311  epttop  14632  cnptoprest  14781  txcnp  14813  metequiv2  15038  cnlimcim  15213  bj-hbalt  15833  bj-intabssel1  15860  decidin  15867  sumdc2  15869  bj-charfunr  15880  bj-axemptylem  15962  bj-nnen2lp  16024  bj-nnord  16028  setindft  16035  bj-inf2vnlem2  16041  bj-inf2vnlem3  16042  bj-inf2vnlem4  16043  exmidsbthrlem  16096  triap  16103  tridceq  16130