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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  454  con2d  633  con3d  640  expi  647  pm3.37  700  pm5.21ndd  717  pm2.37  817  pm2.81  823  dcim  853  condcOLD  866  con4biddc  869  pm2.54dc  903  pm4.79dc  915  pm2.85dc  917  pm3.12dc  971  dn1dc  973  3jao  1342  xoranor  1426  syl6an  1483  syl10  1484  hbald  1544  ax12  1565  hbimd  1626  nfal  1629  19.21ht  1634  19.30dc  1680  19.23t  1729  hbexd  1746  spimth  1788  spimed  1793  cbv2h  1801  cbv2w  1803  equvini  1811  sbiedh  1840  sbcof2  1863  aev  1865  sb3  1884  hbsb2  1889  sbequilem  1891  sbft  1901  sbi1v  1946  cbvexdh  1982  nf5-1  2084  mo23  2128  moexexdc  2171  euexex  2172  exists2  2184  dvelimdc  2413  rsp2  2600  rgen2a  2604  spcimgft  2901  spcimegft  2903  eueq3dc  3000  moeq3dc  3002  reu6  3015  ssddif  3465  reupick2  3519  ifnebibdc  3686  sssnm  3879  prneimg  3899  dfiun2g  4044  exmidsssnc  4342  exmidundifim  4346  opth1  4378  copsexg  4386  opelopabt  4406  issod  4466  sowlin  4467  suctr  4568  reusv3i  4607  ralxfrALT  4615  ssorduni  4636  onintonm  4666  regexmidlem1  4682  nlimsucg  4715  0elnn  4768  ssrelrn  4974  issref  5173  iotaval  5352  fun11iun  5663  brprcneu  5691  fvssunirng  5713  relfvssunirn  5714  fv3  5721  ndmfvg  5729  ssimaex  5767  fvopab3ig  5782  dff4im  5857  ffnfv  5869  fconstfvm  5936  f1mpt  5980  oprabid  6120  mpoeq123  6150  f1o2ndf1  6468  brtposg  6530  rntpos  6533  dftpos4  6539  smores2  6570  tfri3  6643  rdgss  6659  nntri3or  6771  nndifsnid  6785  nnawordex  6807  eroveu  6905  map0g  6974  fundmen  7100  nneneq  7164  fiintim  7244  snon0  7255  fnfi  7256  infnlbti  7372  exmidonfinlem  7551  exmidontri2or  7608  addclpi  7700  enq0tr  7807  genprndl  7894  genprndu  7895  genpdisj  7896  addlocprlem  7908  nqprloc  7918  recexprlemss1l  8008  recexprlemss1u  8009  suplocexprlemss  8088  elrealeu  8202  ltleletr  8413  negf1o  8716  zletric  9697  zlelttric  9698  zltnle  9699  zmulcl  9707  zdcle  9730  zdclt  9731  zeo  9761  uz11  9960  indstr  10008  eqreznegel  10029  negm  10030  lbzbi  10031  fzdcel  10460  fzm1  10523  qletric  10692  qlelttric  10693  qltnle  10694  qdclt  10696  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  qsqeqor  11107  swrdccatin2d  11537  rennim  11789  maxleast  12001  negfi  12016  fsum3cvg  12169  fproddccvg  12363  prodmodc  12369  ndvdssub  12721  bitsinv1lem  12752  algcvgblem  12851  algcvga  12853  isprm3  12920  oddprmdvds  13161  4sqlem2  13196  ballotfilemfc0  13289  ballotfilemfcc  13290  imasaddfnlemg  13693  subrngintm  14628  subrgintm  14659  lmodfopnelem1  14769  islssm  14802  lspsneq0  14871  islidlm  14924  mvrf1fi  15219  epttop  15333  cnptoprest  15482  txcnp  15514  metequiv2  15739  cnlimcim  15914  ppiublem1  16308  umgrclwwlkge2  16865  bj-hbalt  17013  bj-intabssel1  17040  decidin  17047  sumdc2  17049  bj-charfunr  17058  bj-axemptylem  17140  bj-nnen2lp  17202  bj-nnord  17206  setindft  17213  bj-inf2vnlem2  17219  bj-inf2vnlem3  17220  bj-inf2vnlem4  17221  exmidsbthrlem  17290  triap  17301  tridceq  17330