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  syl6ib  161  syl6ibr  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  2813  spcimegft  2815  eueq3dc  2911  moeq3dc  2913  reu6  2926  ssddif  3369  reupick2  3421  sssnm  3754  prneimg  3774  dfiun2g  3918  exmidsssnc  4202  exmidundifim  4206  opth1  4235  copsexg  4243  opelopabt  4261  issod  4318  sowlin  4319  suctr  4420  reusv3i  4458  ralxfrALT  4466  ssorduni  4485  onintonm  4515  regexmidlem1  4531  nlimsucg  4564  0elnn  4617  issref  5010  iotaval  5188  fun11iun  5481  brprcneu  5507  fvssunirng  5529  relfvssunirn  5530  fv3  5537  ndmfvg  5545  ssimaex  5576  fvopab3ig  5589  dff4im  5661  ffnfv  5673  fconstfvm  5733  f1mpt  5769  oprabid  5904  mpoeq123  5931  f1o2ndf1  6226  brtposg  6252  rntpos  6255  dftpos4  6261  smores2  6292  tfri3  6365  rdgss  6381  nntri3or  6491  nndifsnid  6505  nnawordex  6527  eroveu  6623  map0g  6685  fundmen  6803  nneneq  6854  fiintim  6925  snon0  6932  fnfi  6933  infnlbti  7022  exmidonfinlem  7189  exmidontri2or  7239  addclpi  7323  enq0tr  7430  genprndl  7517  genprndu  7518  genpdisj  7519  addlocprlem  7531  nqprloc  7541  recexprlemss1l  7631  recexprlemss1u  7632  suplocexprlemss  7711  elrealeu  7825  ltleletr  8035  negf1o  8335  zletric  9293  zlelttric  9294  zltnle  9295  zmulcl  9302  zdcle  9325  zdclt  9326  zeo  9354  uz11  9546  indstr  9589  eqreznegel  9610  negm  9611  lbzbi  9612  fzdcel  10035  fzm1  10095  qletric  10239  qlelttric  10240  qltnle  10241  frecuzrdgtcl  10407  frecuzrdgfunlem  10414  qsqeqor  10625  rennim  11004  maxleast  11215  negfi  11229  fsum3cvg  11379  fproddccvg  11573  prodmodc  11579  ndvdssub  11927  algcvgblem  12041  algcvga  12043  isprm3  12110  oddprmdvds  12344  4sqlem2  12379  subrgintm  13302  epttop  13461  cnptoprest  13610  txcnp  13642  metequiv2  13867  cnlimcim  14011  bj-hbalt  14375  bj-intabssel1  14402  decidin  14409  sumdc2  14411  bj-charfunr  14422  bj-axemptylem  14504  bj-nnen2lp  14566  bj-nnord  14570  setindft  14577  bj-inf2vnlem2  14583  bj-inf2vnlem3  14584  bj-inf2vnlem4  14585  exmidsbthrlem  14630  triap  14637  tridceq  14664