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  3620  sssnm  3801  prneimg  3821  dfiun2g  3965  exmidsssnc  4255  exmidundifim  4259  opth1  4288  copsexg  4296  opelopabt  4316  issod  4374  sowlin  4375  suctr  4476  reusv3i  4514  ralxfrALT  4522  ssorduni  4543  onintonm  4573  regexmidlem1  4589  nlimsucg  4622  0elnn  4675  ssrelrn  4878  issref  5074  iotaval  5252  fun11iun  5555  brprcneu  5582  fvssunirng  5604  relfvssunirn  5605  fv3  5612  ndmfvg  5620  ssimaex  5653  fvopab3ig  5666  dff4im  5739  ffnfv  5751  fconstfvm  5815  f1mpt  5853  oprabid  5989  mpoeq123  6017  f1o2ndf1  6327  brtposg  6353  rntpos  6356  dftpos4  6362  smores2  6393  tfri3  6466  rdgss  6482  nntri3or  6592  nndifsnid  6606  nnawordex  6628  eroveu  6726  map0g  6788  fundmen  6912  nneneq  6969  fiintim  7043  snon0  7052  fnfi  7053  infnlbti  7143  exmidonfinlem  7317  exmidontri2or  7374  addclpi  7460  enq0tr  7567  genprndl  7654  genprndu  7655  genpdisj  7656  addlocprlem  7668  nqprloc  7678  recexprlemss1l  7768  recexprlemss1u  7769  suplocexprlemss  7848  elrealeu  7962  ltleletr  8174  negf1o  8474  zletric  9436  zlelttric  9437  zltnle  9438  zmulcl  9446  zdcle  9469  zdclt  9470  zeo  9498  uz11  9691  indstr  9734  eqreznegel  9755  negm  9756  lbzbi  9757  fzdcel  10182  fzm1  10242  qletric  10406  qlelttric  10407  qltnle  10408  qdclt  10410  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  qsqeqor  10817  rennim  11388  maxleast  11599  negfi  11614  fsum3cvg  11764  fproddccvg  11958  prodmodc  11964  ndvdssub  12316  bitsinv1lem  12347  algcvgblem  12446  algcvga  12448  isprm3  12515  oddprmdvds  12752  4sqlem2  12787  imasaddfnlemg  13221  subrngintm  14049  subrgintm  14080  lmodfopnelem1  14161  islssm  14194  lspsneq0  14263  islidlm  14316  epttop  14637  cnptoprest  14786  txcnp  14818  metequiv2  15043  cnlimcim  15218  bj-hbalt  15838  bj-intabssel1  15865  decidin  15872  sumdc2  15874  bj-charfunr  15884  bj-axemptylem  15966  bj-nnen2lp  16028  bj-nnord  16032  setindft  16039  bj-inf2vnlem2  16045  bj-inf2vnlem3  16046  bj-inf2vnlem4  16047  exmidsbthrlem  16102  triap  16109  tridceq  16136