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  syl6bi  163  syl6bir  164  pm5.32d  450  con2d  624  con3d  631  expi  638  pm3.37  689  pm5.21ndd  705  pm2.37  805  pm2.81  811  dcim  841  condcOLD  854  con4biddc  857  pm2.54dc  891  pm4.79dc  903  pm2.85dc  905  pm3.12dc  958  dn1dc  960  3jao  1301  xoranor  1377  syl6an  1434  syl10  1435  hbald  1491  ax12  1512  hbimd  1573  nfal  1576  19.21ht  1581  19.30dc  1627  19.23t  1677  hbexd  1694  spimth  1735  spimed  1740  cbv2h  1748  cbv2w  1750  equvini  1758  sbiedh  1787  sbcof2  1810  aev  1812  sb3  1831  hbsb2  1836  sbequilem  1838  sbft  1848  sbi1v  1891  cbvexdh  1926  nf5-1  2024  mo23  2067  moexexdc  2110  euexex  2111  exists2  2123  dvelimdc  2340  rsp2  2527  rgen2a  2531  spcimgft  2814  spcimegft  2816  eueq3dc  2912  moeq3dc  2914  reu6  2927  ssddif  3370  reupick2  3422  sssnm  3755  prneimg  3775  dfiun2g  3919  exmidsssnc  4204  exmidundifim  4208  opth1  4237  copsexg  4245  opelopabt  4263  issod  4320  sowlin  4321  suctr  4422  reusv3i  4460  ralxfrALT  4468  ssorduni  4487  onintonm  4517  regexmidlem1  4533  nlimsucg  4566  0elnn  4619  issref  5012  iotaval  5190  fun11iun  5483  brprcneu  5509  fvssunirng  5531  relfvssunirn  5532  fv3  5539  ndmfvg  5547  ssimaex  5578  fvopab3ig  5591  dff4im  5663  ffnfv  5675  fconstfvm  5735  f1mpt  5772  oprabid  5907  mpoeq123  5934  f1o2ndf1  6229  brtposg  6255  rntpos  6258  dftpos4  6264  smores2  6295  tfri3  6368  rdgss  6384  nntri3or  6494  nndifsnid  6508  nnawordex  6530  eroveu  6626  map0g  6688  fundmen  6806  nneneq  6857  fiintim  6928  snon0  6935  fnfi  6936  infnlbti  7025  exmidonfinlem  7192  exmidontri2or  7242  addclpi  7326  enq0tr  7433  genprndl  7520  genprndu  7521  genpdisj  7522  addlocprlem  7534  nqprloc  7544  recexprlemss1l  7634  recexprlemss1u  7635  suplocexprlemss  7714  elrealeu  7828  ltleletr  8039  negf1o  8339  zletric  9297  zlelttric  9298  zltnle  9299  zmulcl  9306  zdcle  9329  zdclt  9330  zeo  9358  uz11  9550  indstr  9593  eqreznegel  9614  negm  9615  lbzbi  9616  fzdcel  10040  fzm1  10100  qletric  10244  qlelttric  10245  qltnle  10246  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  qsqeqor  10631  rennim  11011  maxleast  11222  negfi  11236  fsum3cvg  11386  fproddccvg  11580  prodmodc  11586  ndvdssub  11935  algcvgblem  12049  algcvga  12051  isprm3  12118  oddprmdvds  12352  4sqlem2  12387  imasaddfnlemg  12735  subrgintm  13364  lmodfopnelem1  13414  epttop  13593  cnptoprest  13742  txcnp  13774  metequiv2  13999  cnlimcim  14143  bj-hbalt  14518  bj-intabssel1  14545  decidin  14552  sumdc2  14554  bj-charfunr  14565  bj-axemptylem  14647  bj-nnen2lp  14709  bj-nnord  14713  setindft  14720  bj-inf2vnlem2  14726  bj-inf2vnlem3  14727  bj-inf2vnlem4  14728  exmidsbthrlem  14773  triap  14780  tridceq  14807