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  629  con3d  636  expi  643  pm3.37  696  pm5.21ndd  713  pm2.37  813  pm2.81  819  dcim  849  condcOLD  862  con4biddc  865  pm2.54dc  899  pm4.79dc  911  pm2.85dc  913  pm3.12dc  967  dn1dc  969  3jao  1338  xoranor  1422  syl6an  1479  syl10  1480  hbald  1540  ax12  1561  hbimd  1622  nfal  1625  19.21ht  1630  19.30dc  1676  19.23t  1725  hbexd  1742  spimth  1784  spimed  1789  cbv2h  1797  cbv2w  1799  equvini  1807  sbiedh  1836  sbcof2  1859  aev  1861  sb3  1880  hbsb2  1885  sbequilem  1887  sbft  1897  sbi1v  1942  cbvexdh  1978  nf5-1  2080  mo23  2124  moexexdc  2167  euexex  2168  exists2  2180  dvelimdc  2407  rsp2  2594  rgen2a  2598  spcimgft  2895  spcimegft  2897  eueq3dc  2993  moeq3dc  2995  reu6  3008  ssddif  3457  reupick2  3509  ifnebibdc  3670  sssnm  3860  prneimg  3880  dfiun2g  4025  exmidsssnc  4318  exmidundifim  4322  opth1  4354  copsexg  4362  opelopabt  4382  issod  4442  sowlin  4443  suctr  4544  reusv3i  4582  ralxfrALT  4590  ssorduni  4611  onintonm  4641  regexmidlem1  4657  nlimsucg  4690  0elnn  4743  ssrelrn  4949  issref  5147  iotaval  5326  fun11iun  5637  brprcneu  5665  fvssunirng  5687  relfvssunirn  5688  fv3  5695  ndmfvg  5703  ssimaex  5740  fvopab3ig  5753  dff4im  5825  ffnfv  5837  fconstfvm  5904  f1mpt  5946  oprabid  6084  mpoeq123  6114  f1o2ndf1  6426  brtposg  6487  rntpos  6490  dftpos4  6496  smores2  6527  tfri3  6600  rdgss  6616  nntri3or  6728  nndifsnid  6742  nnawordex  6764  eroveu  6862  map0g  6924  fundmen  7049  nneneq  7113  fiintim  7193  snon0  7204  fnfi  7205  infnlbti  7319  exmidonfinlem  7498  exmidontri2or  7555  addclpi  7644  enq0tr  7751  genprndl  7838  genprndu  7839  genpdisj  7840  addlocprlem  7852  nqprloc  7862  recexprlemss1l  7952  recexprlemss1u  7953  suplocexprlemss  8032  elrealeu  8146  ltleletr  8357  negf1o  8657  zletric  9623  zlelttric  9624  zltnle  9625  zmulcl  9633  zdcle  9656  zdclt  9657  zeo  9686  uz11  9880  indstr  9928  eqreznegel  9949  negm  9950  lbzbi  9951  fzdcel  10377  fzm1  10438  qletric  10605  qlelttric  10606  qltnle  10607  qdclt  10609  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  qsqeqor  11016  swrdccatin2d  11440  rennim  11691  maxleast  11902  negfi  11917  fsum3cvg  12068  fproddccvg  12262  prodmodc  12268  ndvdssub  12620  bitsinv1lem  12651  algcvgblem  12750  algcvga  12752  isprm3  12819  oddprmdvds  13056  4sqlem2  13091  ballotfilemfc0  13153  ballotfilemfcc  13154  imasaddfnlemg  13544  subrngintm  14374  subrgintm  14405  lmodfopnelem1  14489  islssm  14522  lspsneq0  14591  islidlm  14644  epttop  14972  cnptoprest  15121  txcnp  15153  metequiv2  15378  cnlimcim  15553  umgrclwwlkge2  16414  bj-hbalt  16552  bj-intabssel1  16579  decidin  16586  sumdc2  16588  bj-charfunr  16597  bj-axemptylem  16679  bj-nnen2lp  16741  bj-nnord  16745  setindft  16752  bj-inf2vnlem2  16758  bj-inf2vnlem3  16759  bj-inf2vnlem4  16760  exmidsbthrlem  16819  triap  16830  tridceq  16858