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  690  pm5.21ndd  706  pm2.37  806  pm2.81  812  dcim  842  condcOLD  855  con4biddc  858  pm2.54dc  892  pm4.79dc  904  pm2.85dc  906  pm3.12dc  960  dn1dc  962  3jao  1313  xoranor  1396  syl6an  1453  syl10  1454  hbald  1513  ax12  1534  hbimd  1595  nfal  1598  19.21ht  1603  19.30dc  1649  19.23t  1699  hbexd  1716  spimth  1757  spimed  1762  cbv2h  1770  cbv2w  1772  equvini  1780  sbiedh  1809  sbcof2  1832  aev  1834  sb3  1853  hbsb2  1858  sbequilem  1860  sbft  1870  sbi1v  1914  cbvexdh  1949  nf5-1  2051  mo23  2094  moexexdc  2137  euexex  2138  exists2  2150  dvelimdc  2368  rsp2  2555  rgen2a  2559  spcimgft  2848  spcimegft  2850  eueq3dc  2946  moeq3dc  2948  reu6  2961  ssddif  3406  reupick2  3458  ifnebibdc  3614  sssnm  3794  prneimg  3814  dfiun2g  3958  exmidsssnc  4246  exmidundifim  4250  opth1  4279  copsexg  4287  opelopabt  4307  issod  4365  sowlin  4366  suctr  4467  reusv3i  4505  ralxfrALT  4513  ssorduni  4534  onintonm  4564  regexmidlem1  4580  nlimsucg  4613  0elnn  4666  issref  5064  iotaval  5242  fun11iun  5542  brprcneu  5568  fvssunirng  5590  relfvssunirn  5591  fv3  5598  ndmfvg  5606  ssimaex  5639  fvopab3ig  5652  dff4im  5725  ffnfv  5737  fconstfvm  5801  f1mpt  5839  oprabid  5975  mpoeq123  6003  f1o2ndf1  6313  brtposg  6339  rntpos  6342  dftpos4  6348  smores2  6379  tfri3  6452  rdgss  6468  nntri3or  6578  nndifsnid  6592  nnawordex  6614  eroveu  6712  map0g  6774  fundmen  6897  nneneq  6953  fiintim  7027  snon0  7036  fnfi  7037  infnlbti  7127  exmidonfinlem  7300  exmidontri2or  7354  addclpi  7439  enq0tr  7546  genprndl  7633  genprndu  7634  genpdisj  7635  addlocprlem  7647  nqprloc  7657  recexprlemss1l  7747  recexprlemss1u  7748  suplocexprlemss  7827  elrealeu  7941  ltleletr  8153  negf1o  8453  zletric  9415  zlelttric  9416  zltnle  9417  zmulcl  9425  zdcle  9448  zdclt  9449  zeo  9477  uz11  9670  indstr  9713  eqreznegel  9734  negm  9735  lbzbi  9736  fzdcel  10161  fzm1  10221  qletric  10382  qlelttric  10383  qltnle  10384  qdclt  10386  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  qsqeqor  10793  rennim  11284  maxleast  11495  negfi  11510  fsum3cvg  11660  fproddccvg  11854  prodmodc  11860  ndvdssub  12212  bitsinv1lem  12243  algcvgblem  12342  algcvga  12344  isprm3  12411  oddprmdvds  12648  4sqlem2  12683  imasaddfnlemg  13117  subrngintm  13945  subrgintm  13976  lmodfopnelem1  14057  islssm  14090  lspsneq0  14159  islidlm  14212  epttop  14533  cnptoprest  14682  txcnp  14714  metequiv2  14939  cnlimcim  15114  bj-hbalt  15661  bj-intabssel1  15688  decidin  15695  sumdc2  15697  bj-charfunr  15708  bj-axemptylem  15790  bj-nnen2lp  15852  bj-nnord  15856  setindft  15863  bj-inf2vnlem2  15869  bj-inf2vnlem3  15870  bj-inf2vnlem4  15871  exmidsbthrlem  15923  triap  15930  tridceq  15957