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  1783  spimed  1788  cbv2h  1796  cbv2w  1798  equvini  1806  sbiedh  1835  sbcof2  1858  aev  1860  sb3  1879  hbsb2  1884  sbequilem  1886  sbft  1896  sbi1v  1940  cbvexdh  1975  nf5-1  2077  mo23  2121  moexexdc  2164  euexex  2165  exists2  2177  dvelimdc  2396  rsp2  2583  rgen2a  2587  spcimgft  2883  spcimegft  2885  eueq3dc  2981  moeq3dc  2983  reu6  2996  ssddif  3443  reupick2  3495  ifnebibdc  3655  sssnm  3842  prneimg  3862  dfiun2g  4007  exmidsssnc  4299  exmidundifim  4303  opth1  4334  copsexg  4342  opelopabt  4362  issod  4422  sowlin  4423  suctr  4524  reusv3i  4562  ralxfrALT  4570  ssorduni  4591  onintonm  4621  regexmidlem1  4637  nlimsucg  4670  0elnn  4723  ssrelrn  4928  issref  5126  iotaval  5305  fun11iun  5613  brprcneu  5641  fvssunirng  5663  relfvssunirn  5664  fv3  5671  ndmfvg  5679  ssimaex  5716  fvopab3ig  5729  dff4im  5801  ffnfv  5813  fconstfvm  5880  f1mpt  5922  oprabid  6060  mpoeq123  6090  f1o2ndf1  6402  brtposg  6463  rntpos  6466  dftpos4  6472  smores2  6503  tfri3  6576  rdgss  6592  nntri3or  6704  nndifsnid  6718  nnawordex  6740  eroveu  6838  map0g  6900  fundmen  7024  nneneq  7086  fiintim  7166  snon0  7177  fnfi  7178  infnlbti  7268  exmidonfinlem  7447  exmidontri2or  7504  addclpi  7590  enq0tr  7697  genprndl  7784  genprndu  7785  genpdisj  7786  addlocprlem  7798  nqprloc  7808  recexprlemss1l  7898  recexprlemss1u  7899  suplocexprlemss  7978  elrealeu  8092  ltleletr  8303  negf1o  8603  zletric  9567  zlelttric  9568  zltnle  9569  zmulcl  9577  zdcle  9600  zdclt  9601  zeo  9629  uz11  9823  indstr  9871  eqreznegel  9892  negm  9893  lbzbi  9894  fzdcel  10320  fzm1  10380  qletric  10547  qlelttric  10548  qltnle  10549  qdclt  10551  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  qsqeqor  10958  swrdccatin2d  11374  rennim  11625  maxleast  11836  negfi  11851  fsum3cvg  12002  fproddccvg  12196  prodmodc  12202  ndvdssub  12554  bitsinv1lem  12585  algcvgblem  12684  algcvga  12686  isprm3  12753  oddprmdvds  12990  4sqlem2  13025  imasaddfnlemg  13460  subrngintm  14290  subrgintm  14321  lmodfopnelem1  14403  islssm  14436  lspsneq0  14505  islidlm  14558  epttop  14884  cnptoprest  15033  txcnp  15065  metequiv2  15290  cnlimcim  15465  umgrclwwlkge2  16326  bj-hbalt  16464  bj-intabssel1  16491  decidin  16498  sumdc2  16500  bj-charfunr  16509  bj-axemptylem  16591  bj-nnen2lp  16653  bj-nnord  16657  setindft  16664  bj-inf2vnlem2  16670  bj-inf2vnlem3  16671  bj-inf2vnlem4  16672  exmidsbthrlem  16733  triap  16744  tridceq  16772