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  1312  xoranor  1388  syl6an  1445  syl10  1446  hbald  1505  ax12  1526  hbimd  1587  nfal  1590  19.21ht  1595  19.30dc  1641  19.23t  1691  hbexd  1708  spimth  1749  spimed  1754  cbv2h  1762  cbv2w  1764  equvini  1772  sbiedh  1801  sbcof2  1824  aev  1826  sb3  1845  hbsb2  1850  sbequilem  1852  sbft  1862  sbi1v  1906  cbvexdh  1941  nf5-1  2043  mo23  2086  moexexdc  2129  euexex  2130  exists2  2142  dvelimdc  2360  rsp2  2547  rgen2a  2551  spcimgft  2840  spcimegft  2842  eueq3dc  2938  moeq3dc  2940  reu6  2953  ssddif  3397  reupick2  3449  ifnebibdc  3604  sssnm  3784  prneimg  3804  dfiun2g  3948  exmidsssnc  4236  exmidundifim  4240  opth1  4269  copsexg  4277  opelopabt  4296  issod  4354  sowlin  4355  suctr  4456  reusv3i  4494  ralxfrALT  4502  ssorduni  4523  onintonm  4553  regexmidlem1  4569  nlimsucg  4602  0elnn  4655  issref  5052  iotaval  5230  fun11iun  5525  brprcneu  5551  fvssunirng  5573  relfvssunirn  5574  fv3  5581  ndmfvg  5589  ssimaex  5622  fvopab3ig  5635  dff4im  5708  ffnfv  5720  fconstfvm  5780  f1mpt  5818  oprabid  5954  mpoeq123  5981  f1o2ndf1  6286  brtposg  6312  rntpos  6315  dftpos4  6321  smores2  6352  tfri3  6425  rdgss  6441  nntri3or  6551  nndifsnid  6565  nnawordex  6587  eroveu  6685  map0g  6747  fundmen  6865  nneneq  6918  fiintim  6992  snon0  7001  fnfi  7002  infnlbti  7092  exmidonfinlem  7260  exmidontri2or  7310  addclpi  7394  enq0tr  7501  genprndl  7588  genprndu  7589  genpdisj  7590  addlocprlem  7602  nqprloc  7612  recexprlemss1l  7702  recexprlemss1u  7703  suplocexprlemss  7782  elrealeu  7896  ltleletr  8108  negf1o  8408  zletric  9370  zlelttric  9371  zltnle  9372  zmulcl  9379  zdcle  9402  zdclt  9403  zeo  9431  uz11  9624  indstr  9667  eqreznegel  9688  negm  9689  lbzbi  9690  fzdcel  10115  fzm1  10175  qletric  10331  qlelttric  10332  qltnle  10333  qdclt  10335  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  qsqeqor  10742  rennim  11167  maxleast  11378  negfi  11393  fsum3cvg  11543  fproddccvg  11737  prodmodc  11743  ndvdssub  12095  algcvgblem  12217  algcvga  12219  isprm3  12286  oddprmdvds  12523  4sqlem2  12558  imasaddfnlemg  12957  subrngintm  13768  subrgintm  13799  lmodfopnelem1  13880  islssm  13913  lspsneq0  13982  islidlm  14035  epttop  14326  cnptoprest  14475  txcnp  14507  metequiv2  14732  cnlimcim  14907  bj-hbalt  15409  bj-intabssel1  15436  decidin  15443  sumdc2  15445  bj-charfunr  15456  bj-axemptylem  15538  bj-nnen2lp  15600  bj-nnord  15604  setindft  15611  bj-inf2vnlem2  15617  bj-inf2vnlem3  15618  bj-inf2vnlem4  15619  exmidsbthrlem  15666  triap  15673  tridceq  15700