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  629  con3d  636  expi  643  pm3.37  696  pm5.21ndd  713  pm2.37  813  pm2.81  819  dcim  849  condcOLD  862  con4biddc  865  pm2.54dc  899  pm4.79dc  911  pm2.85dc  913  pm3.12dc  967  dn1dc  969  3jao  1338  xoranor  1422  syl6an  1479  syl10  1480  hbald  1540  ax12  1561  hbimd  1622  nfal  1625  19.21ht  1630  19.30dc  1676  19.23t  1725  hbexd  1742  spimth  1784  spimed  1789  cbv2h  1797  cbv2w  1799  equvini  1807  sbiedh  1836  sbcof2  1859  aev  1861  sb3  1880  hbsb2  1885  sbequilem  1887  sbft  1897  sbi1v  1941  cbvexdh  1976  nf5-1  2078  mo23  2122  moexexdc  2165  euexex  2166  exists2  2178  dvelimdc  2405  rsp2  2592  rgen2a  2596  spcimgft  2893  spcimegft  2895  eueq3dc  2991  moeq3dc  2993  reu6  3006  ssddif  3455  reupick2  3507  ifnebibdc  3668  sssnm  3858  prneimg  3878  dfiun2g  4023  exmidsssnc  4316  exmidundifim  4320  opth1  4352  copsexg  4360  opelopabt  4380  issod  4440  sowlin  4441  suctr  4542  reusv3i  4580  ralxfrALT  4588  ssorduni  4609  onintonm  4639  regexmidlem1  4655  nlimsucg  4688  0elnn  4741  ssrelrn  4947  issref  5145  iotaval  5324  fun11iun  5635  brprcneu  5663  fvssunirng  5685  relfvssunirn  5686  fv3  5693  ndmfvg  5701  ssimaex  5738  fvopab3ig  5751  dff4im  5823  ffnfv  5835  fconstfvm  5902  f1mpt  5944  oprabid  6082  mpoeq123  6112  f1o2ndf1  6424  brtposg  6485  rntpos  6488  dftpos4  6494  smores2  6525  tfri3  6598  rdgss  6614  nntri3or  6726  nndifsnid  6740  nnawordex  6762  eroveu  6860  map0g  6922  fundmen  7047  nneneq  7111  fiintim  7191  snon0  7202  fnfi  7203  infnlbti  7317  exmidonfinlem  7496  exmidontri2or  7553  addclpi  7642  enq0tr  7749  genprndl  7836  genprndu  7837  genpdisj  7838  addlocprlem  7850  nqprloc  7860  recexprlemss1l  7950  recexprlemss1u  7951  suplocexprlemss  8030  elrealeu  8144  ltleletr  8355  negf1o  8655  zletric  9621  zlelttric  9622  zltnle  9623  zmulcl  9631  zdcle  9654  zdclt  9655  zeo  9683  uz11  9877  indstr  9925  eqreznegel  9946  negm  9947  lbzbi  9948  fzdcel  10374  fzm1  10434  qletric  10601  qlelttric  10602  qltnle  10603  qdclt  10605  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  qsqeqor  11012  swrdccatin2d  11436  rennim  11687  maxleast  11898  negfi  11913  fsum3cvg  12064  fproddccvg  12258  prodmodc  12264  ndvdssub  12616  bitsinv1lem  12647  algcvgblem  12746  algcvga  12748  isprm3  12815  oddprmdvds  13052  4sqlem2  13087  imasaddfnlemg  13527  subrngintm  14357  subrgintm  14388  lmodfopnelem1  14472  islssm  14505  lspsneq0  14574  islidlm  14627  epttop  14955  cnptoprest  15104  txcnp  15136  metequiv2  15361  cnlimcim  15536  umgrclwwlkge2  16397  bj-hbalt  16535  bj-intabssel1  16562  decidin  16569  sumdc2  16571  bj-charfunr  16580  bj-axemptylem  16662  bj-nnen2lp  16724  bj-nnord  16728  setindft  16735  bj-inf2vnlem2  16741  bj-inf2vnlem3  16742  bj-inf2vnlem4  16743  exmidsbthrlem  16802  triap  16813  tridceq  16841