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  6529  rntpos  6532  dftpos4  6538  smores2  6569  tfri3  6642  rdgss  6658  nntri3or  6770  nndifsnid  6784  nnawordex  6806  eroveu  6904  map0g  6973  fundmen  7098  nneneq  7162  fiintim  7242  snon0  7253  fnfi  7254  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  9699  zlelttric  9700  zltnle  9701  zmulcl  9709  zdcle  9732  zdclt  9733  zeo  9762  uz11  9961  indstr  10009  eqreznegel  10030  negm  10031  lbzbi  10032  fzdcel  10461  fzm1  10524  qletric  10693  qlelttric  10694  qltnle  10695  qdclt  10697  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  qsqeqor  11108  swrdccatin2d  11538  rennim  11790  maxleast  12002  negfi  12017  fsum3cvg  12170  fproddccvg  12364  prodmodc  12370  ndvdssub  12722  bitsinv1lem  12753  algcvgblem  12852  algcvga  12854  isprm3  12921  oddprmdvds  13162  4sqlem2  13197  ballotfilemfc0  13290  ballotfilemfcc  13291  imasaddfnlemg  13694  subrngintm  14629  subrgintm  14660  lmodfopnelem1  14770  islssm  14803  lspsneq0  14872  islidlm  14925  epttop  15316  cnptoprest  15465  txcnp  15497  metequiv2  15722  cnlimcim  15897  ppiublem1  16291  umgrclwwlkge2  16848  bj-hbalt  16996  bj-intabssel1  17023  decidin  17030  sumdc2  17032  bj-charfunr  17041  bj-axemptylem  17123  bj-nnen2lp  17185  bj-nnord  17189  setindft  17196  bj-inf2vnlem2  17202  bj-inf2vnlem3  17203  bj-inf2vnlem4  17204  exmidsbthrlem  17273  triap  17284  tridceq  17313