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  11255  maxleast  11466  negfi  11481  fsum3cvg  11631  fproddccvg  11825  prodmodc  11831  ndvdssub  12183  bitsinv1lem  12214  algcvgblem  12313  algcvga  12315  isprm3  12382  oddprmdvds  12619  4sqlem2  12654  imasaddfnlemg  13088  subrngintm  13916  subrgintm  13947  lmodfopnelem1  14028  islssm  14061  lspsneq0  14130  islidlm  14183  epttop  14504  cnptoprest  14653  txcnp  14685  metequiv2  14910  cnlimcim  15085  bj-hbalt  15632  bj-intabssel1  15659  decidin  15666  sumdc2  15668  bj-charfunr  15679  bj-axemptylem  15761  bj-nnen2lp  15823  bj-nnord  15827  setindft  15834  bj-inf2vnlem2  15840  bj-inf2vnlem3  15841  bj-inf2vnlem4  15842  exmidsbthrlem  15894  triap  15901  tridceq  15928