Theorem syl6 29

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 25	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl56  30  syl6com  31  a1dd  42  syl6mpi  58  syl6c  60  com34  77  ex  108  syl6ib  150  syl6ibr  151  syl6bi  152  syl6bir  153  pm5.32d  423  con2d  554  con3d  561  expi  567  pm5.21ndd  621  pm2.37  718  pm2.81  724  condc  749  con4biddc  754  dcim  784  pm2.54dc  790  pm4.79dc  809  pm2.85dc  811  pm3.12dc  865  dn1dc  867  3jao  1196  xoranor  1268  syl6an  1323  syl10  1324  hbald  1380  ax-12  1402  hbimd  1465  19.21ht  1473  19.30dc  1518  19.23t  1567  hbexd  1584  spimth  1623  spimed  1628  cbv2h  1634  equvini  1641  sbiedh  1670  sbcof2  1691  aev  1693  sb3  1712  hbsb2  1717  sbequilem  1719  sbft  1728  sbi1v  1771  cbvexdh  1801  mo23  1941  moexexdc  1984  euexex  1985  exists2  1997  dvelimdc  2197  rsp2  2371  rgen2a  2375  spcimgft  2629  spcimegft  2631  eueq3dc  2715  moeq3dc  2717  reu6  2730  ssddif  3171  reupick2  3223  sssnm  3525  prneimg  3545  dfiun2g  3689  opth1  3973  copsexg  3981  opelopabt  3999  issod  4056  sowlin  4057  suctr  4158  reusv3i  4191  ralxfrALT  4199  ssorduni  4213  onintonm  4243  regexmidlem1  4258  nlimsucg  4290  0elnn  4340  issref  4707  iotaval  4878  fun11iun  5147  brprcneu  5171  fvssunirng  5190  relfvssunirn  5191  fv3  5197  ndmfvg  5204  ssimaex  5234  fvopab3ig  5246  dff4im  5313  ffnfv  5323  fconstfvm  5379  f1mpt  5410  oprabid  5537  mpt2eq123  5564  f1o2ndf1  5849  brtposg  5869  rntpos  5872  dftpos4  5878  smores2  5909  tfr0  5937  tfri3  5953  rdgss  5970  rdgon  5973  nntri3or  6072  nnawordex  6101  eroveu  6197  fundmen  6286  nneneq  6320  snon0  6356  addclpi  6425  enq0tr  6532  genprndl  6619  genprndu  6620  genpdisj  6621  addlocprlem  6633  nqprloc  6643  recexprlemss1l  6733  recexprlemss1u  6734  elrealeu  6906  ltleletr  7100  zletric  8289  zlelttric  8290  zltnle  8291  zmulcl  8297  zdcle  8317  zdclt  8318  zeo  8343  uz11  8495  indstr  8536  eqreznegel  8549  negm  8550  lbzbi  8551  fzdcel  8904  fzm1  8962  qletric  9099  qlelttric  9100  qltnle  9101  frecuzrdgfn  9198  rennim  9600  algcvgblem  9888  ialgcvga  9890  bj-hbalt  9903  bj-intabssel1  9929  bj-axemptylem  10012  bj-nnen2lp  10079  bj-nnord  10083  setindft  10090  bj-inf2vnlem2  10096  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098