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  627  con3d  634  expi  641  pm3.37  693  pm5.21ndd  710  pm2.37  810  pm2.81  816  dcim  846  condcOLD  859  con4biddc  862  pm2.54dc  896  pm4.79dc  908  pm2.85dc  910  pm3.12dc  964  dn1dc  966  3jao  1335  xoranor  1419  syl6an  1476  syl10  1477  hbald  1537  ax12  1558  hbimd  1619  nfal  1622  19.21ht  1627  19.30dc  1673  19.23t  1723  hbexd  1740  spimth  1781  spimed  1786  cbv2h  1794  cbv2w  1796  equvini  1804  sbiedh  1833  sbcof2  1856  aev  1858  sb3  1877  hbsb2  1882  sbequilem  1884  sbft  1894  sbi1v  1938  cbvexdh  1973  nf5-1  2075  mo23  2119  moexexdc  2162  euexex  2163  exists2  2175  dvelimdc  2393  rsp2  2580  rgen2a  2584  spcimgft  2879  spcimegft  2881  eueq3dc  2977  moeq3dc  2979  reu6  2992  ssddif  3438  reupick2  3490  ifnebibdc  3648  sssnm  3831  prneimg  3851  dfiun2g  3996  exmidsssnc  4286  exmidundifim  4290  opth1  4321  copsexg  4329  opelopabt  4349  issod  4409  sowlin  4410  suctr  4511  reusv3i  4549  ralxfrALT  4557  ssorduni  4578  onintonm  4608  regexmidlem1  4624  nlimsucg  4657  0elnn  4710  ssrelrn  4913  issref  5110  iotaval  5289  fun11iun  5592  brprcneu  5619  fvssunirng  5641  relfvssunirn  5642  fv3  5649  ndmfvg  5657  ssimaex  5694  fvopab3ig  5707  dff4im  5780  ffnfv  5792  fconstfvm  5856  f1mpt  5894  oprabid  6032  mpoeq123  6062  f1o2ndf1  6372  brtposg  6398  rntpos  6401  dftpos4  6407  smores2  6438  tfri3  6511  rdgss  6527  nntri3or  6637  nndifsnid  6651  nnawordex  6673  eroveu  6771  map0g  6833  fundmen  6957  nneneq  7014  fiintim  7089  snon0  7098  fnfi  7099  infnlbti  7189  exmidonfinlem  7367  exmidontri2or  7424  addclpi  7510  enq0tr  7617  genprndl  7704  genprndu  7705  genpdisj  7706  addlocprlem  7718  nqprloc  7728  recexprlemss1l  7818  recexprlemss1u  7819  suplocexprlemss  7898  elrealeu  8012  ltleletr  8224  negf1o  8524  zletric  9486  zlelttric  9487  zltnle  9488  zmulcl  9496  zdcle  9519  zdclt  9520  zeo  9548  uz11  9741  indstr  9784  eqreznegel  9805  negm  9806  lbzbi  9807  fzdcel  10232  fzm1  10292  qletric  10456  qlelttric  10457  qltnle  10458  qdclt  10460  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  qsqeqor  10867  swrdccatin2d  11271  rennim  11508  maxleast  11719  negfi  11734  fsum3cvg  11884  fproddccvg  12078  prodmodc  12084  ndvdssub  12436  bitsinv1lem  12467  algcvgblem  12566  algcvga  12568  isprm3  12635  oddprmdvds  12872  4sqlem2  12907  imasaddfnlemg  13342  subrngintm  14170  subrgintm  14201  lmodfopnelem1  14282  islssm  14315  lspsneq0  14384  islidlm  14437  epttop  14758  cnptoprest  14907  txcnp  14939  metequiv2  15164  cnlimcim  15339  bj-hbalt  16085  bj-intabssel1  16112  decidin  16119  sumdc2  16121  bj-charfunr  16131  bj-axemptylem  16213  bj-nnen2lp  16275  bj-nnord  16279  setindft  16286  bj-inf2vnlem2  16292  bj-inf2vnlem3  16293  bj-inf2vnlem4  16294  exmidsbthrlem  16349  triap  16356  tridceq  16383