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  114  syl6ib  160  syl6ibr  161  syl6bi  162  syl6bir  163  pm5.32d  446  con2d  614  con3d  621  expi  628  pm3.37  679  pm5.21ndd  695  pm2.37  795  pm2.81  801  dcim  831  condcOLD  844  con4biddc  847  pm2.54dc  881  pm4.79dc  893  pm2.85dc  895  pm3.12dc  948  dn1dc  950  3jao  1291  xoranor  1367  syl6an  1422  syl10  1423  hbald  1479  ax12  1500  hbimd  1561  nfal  1564  19.21ht  1569  19.30dc  1615  19.23t  1665  hbexd  1682  spimth  1723  spimed  1728  cbv2h  1736  cbv2w  1738  equvini  1746  sbiedh  1775  sbcof2  1798  aev  1800  sb3  1819  hbsb2  1824  sbequilem  1826  sbft  1836  sbi1v  1879  cbvexdh  1914  nf5-1  2012  mo23  2055  moexexdc  2098  euexex  2099  exists2  2111  dvelimdc  2329  rsp2  2516  rgen2a  2520  spcimgft  2802  spcimegft  2804  eueq3dc  2900  moeq3dc  2902  reu6  2915  ssddif  3356  reupick2  3408  sssnm  3734  prneimg  3754  dfiun2g  3898  exmidsssnc  4182  exmidundifim  4186  opth1  4214  copsexg  4222  opelopabt  4240  issod  4297  sowlin  4298  suctr  4399  reusv3i  4437  ralxfrALT  4445  ssorduni  4464  onintonm  4494  regexmidlem1  4510  nlimsucg  4543  0elnn  4596  issref  4986  iotaval  5164  fun11iun  5453  brprcneu  5479  fvssunirng  5501  relfvssunirn  5502  fv3  5509  ndmfvg  5517  ssimaex  5547  fvopab3ig  5560  dff4im  5631  ffnfv  5643  fconstfvm  5703  f1mpt  5739  oprabid  5874  mpoeq123  5901  f1o2ndf1  6196  brtposg  6222  rntpos  6225  dftpos4  6231  smores2  6262  tfri3  6335  rdgss  6351  nntri3or  6461  nndifsnid  6475  nnawordex  6496  eroveu  6592  map0g  6654  fundmen  6772  nneneq  6823  fiintim  6894  snon0  6901  fnfi  6902  infnlbti  6991  exmidonfinlem  7149  exmidontri2or  7199  addclpi  7268  enq0tr  7375  genprndl  7462  genprndu  7463  genpdisj  7464  addlocprlem  7476  nqprloc  7486  recexprlemss1l  7576  recexprlemss1u  7577  suplocexprlemss  7656  elrealeu  7770  ltleletr  7980  negf1o  8280  zletric  9235  zlelttric  9236  zltnle  9237  zmulcl  9244  zdcle  9267  zdclt  9268  zeo  9296  uz11  9488  indstr  9531  eqreznegel  9552  negm  9553  lbzbi  9554  fzdcel  9975  fzm1  10035  qletric  10179  qlelttric  10180  qltnle  10181  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  qsqeqor  10565  rennim  10944  maxleast  11155  negfi  11169  fsum3cvg  11319  fproddccvg  11513  prodmodc  11519  ndvdssub  11867  algcvgblem  11981  algcvga  11983  isprm3  12050  oddprmdvds  12284  4sqlem2  12319  epttop  12730  cnptoprest  12879  txcnp  12911  metequiv2  13136  cnlimcim  13280  bj-hbalt  13644  bj-intabssel1  13671  decidin  13678  sumdc2  13680  bj-charfunr  13692  bj-axemptylem  13774  bj-nnen2lp  13836  bj-nnord  13840  setindft  13847  bj-inf2vnlem2  13853  bj-inf2vnlem3  13854  bj-inf2vnlem4  13855  exmidsbthrlem  13901  triap  13908  tridceq  13935