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  2813  spcimegft  2815  eueq3dc  2911  moeq3dc  2913  reu6  2926  ssddif  3369  reupick2  3421  sssnm  3754  prneimg  3774  dfiun2g  3918  exmidsssnc  4203  exmidundifim  4207  opth1  4236  copsexg  4244  opelopabt  4262  issod  4319  sowlin  4320  suctr  4421  reusv3i  4459  ralxfrALT  4467  ssorduni  4486  onintonm  4516  regexmidlem1  4532  nlimsucg  4565  0elnn  4618  issref  5011  iotaval  5189  fun11iun  5482  brprcneu  5508  fvssunirng  5530  relfvssunirn  5531  fv3  5538  ndmfvg  5546  ssimaex  5577  fvopab3ig  5590  dff4im  5662  ffnfv  5674  fconstfvm  5734  f1mpt  5771  oprabid  5906  mpoeq123  5933  f1o2ndf1  6228  brtposg  6254  rntpos  6257  dftpos4  6263  smores2  6294  tfri3  6367  rdgss  6383  nntri3or  6493  nndifsnid  6507  nnawordex  6529  eroveu  6625  map0g  6687  fundmen  6805  nneneq  6856  fiintim  6927  snon0  6934  fnfi  6935  infnlbti  7024  exmidonfinlem  7191  exmidontri2or  7241  addclpi  7325  enq0tr  7432  genprndl  7519  genprndu  7520  genpdisj  7521  addlocprlem  7533  nqprloc  7543  recexprlemss1l  7633  recexprlemss1u  7634  suplocexprlemss  7713  elrealeu  7827  ltleletr  8038  negf1o  8338  zletric  9296  zlelttric  9297  zltnle  9298  zmulcl  9305  zdcle  9328  zdclt  9329  zeo  9357  uz11  9549  indstr  9592  eqreznegel  9613  negm  9614  lbzbi  9615  fzdcel  10039  fzm1  10099  qletric  10243  qlelttric  10244  qltnle  10245  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  qsqeqor  10630  rennim  11010  maxleast  11221  negfi  11235  fsum3cvg  11385  fproddccvg  11579  prodmodc  11585  ndvdssub  11934  algcvgblem  12048  algcvga  12050  isprm3  12117  oddprmdvds  12351  4sqlem2  12386  imasaddfnlemg  12734  subrgintm  13362  epttop  13560  cnptoprest  13709  txcnp  13741  metequiv2  13966  cnlimcim  14110  bj-hbalt  14485  bj-intabssel1  14512  decidin  14519  sumdc2  14521  bj-charfunr  14532  bj-axemptylem  14614  bj-nnen2lp  14676  bj-nnord  14680  setindft  14687  bj-inf2vnlem2  14693  bj-inf2vnlem3  14694  bj-inf2vnlem4  14695  exmidsbthrlem  14740  triap  14747  tridceq  14774