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  695  pm5.21ndd  712  pm2.37  812  pm2.81  818  dcim  848  condcOLD  861  con4biddc  864  pm2.54dc  898  pm4.79dc  910  pm2.85dc  912  pm3.12dc  966  dn1dc  968  3jao  1337  xoranor  1421  syl6an  1478  syl10  1479  hbald  1539  ax12  1560  hbimd  1621  nfal  1624  19.21ht  1629  19.30dc  1675  19.23t  1725  hbexd  1742  spimth  1783  spimed  1788  cbv2h  1796  cbv2w  1798  equvini  1806  sbiedh  1835  sbcof2  1858  aev  1860  sb3  1879  hbsb2  1884  sbequilem  1886  sbft  1896  sbi1v  1940  cbvexdh  1975  nf5-1  2077  mo23  2121  moexexdc  2164  euexex  2165  exists2  2177  dvelimdc  2395  rsp2  2582  rgen2a  2586  spcimgft  2882  spcimegft  2884  eueq3dc  2980  moeq3dc  2982  reu6  2995  ssddif  3441  reupick2  3493  ifnebibdc  3651  sssnm  3837  prneimg  3857  dfiun2g  4002  exmidsssnc  4293  exmidundifim  4297  opth1  4328  copsexg  4336  opelopabt  4356  issod  4416  sowlin  4417  suctr  4518  reusv3i  4556  ralxfrALT  4564  ssorduni  4585  onintonm  4615  regexmidlem1  4631  nlimsucg  4664  0elnn  4717  ssrelrn  4922  issref  5119  iotaval  5298  fun11iun  5604  brprcneu  5632  fvssunirng  5654  relfvssunirn  5655  fv3  5662  ndmfvg  5670  ssimaex  5707  fvopab3ig  5720  dff4im  5793  ffnfv  5805  fconstfvm  5871  f1mpt  5911  oprabid  6049  mpoeq123  6079  f1o2ndf1  6392  brtposg  6419  rntpos  6422  dftpos4  6428  smores2  6459  tfri3  6532  rdgss  6548  nntri3or  6660  nndifsnid  6674  nnawordex  6696  eroveu  6794  map0g  6856  fundmen  6980  nneneq  7042  fiintim  7122  snon0  7133  fnfi  7134  infnlbti  7224  exmidonfinlem  7403  exmidontri2or  7460  addclpi  7546  enq0tr  7653  genprndl  7740  genprndu  7741  genpdisj  7742  addlocprlem  7754  nqprloc  7764  recexprlemss1l  7854  recexprlemss1u  7855  suplocexprlemss  7934  elrealeu  8048  ltleletr  8260  negf1o  8560  zletric  9522  zlelttric  9523  zltnle  9524  zmulcl  9532  zdcle  9555  zdclt  9556  zeo  9584  uz11  9778  indstr  9826  eqreznegel  9847  negm  9848  lbzbi  9849  fzdcel  10274  fzm1  10334  qletric  10500  qlelttric  10501  qltnle  10502  qdclt  10504  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  qsqeqor  10911  swrdccatin2d  11324  rennim  11562  maxleast  11773  negfi  11788  fsum3cvg  11938  fproddccvg  12132  prodmodc  12138  ndvdssub  12490  bitsinv1lem  12521  algcvgblem  12620  algcvga  12622  isprm3  12689  oddprmdvds  12926  4sqlem2  12961  imasaddfnlemg  13396  subrngintm  14225  subrgintm  14256  lmodfopnelem1  14337  islssm  14370  lspsneq0  14439  islidlm  14492  epttop  14813  cnptoprest  14962  txcnp  14994  metequiv2  15219  cnlimcim  15394  umgrclwwlkge2  16252  bj-hbalt  16359  bj-intabssel1  16386  decidin  16393  sumdc2  16395  bj-charfunr  16405  bj-axemptylem  16487  bj-nnen2lp  16549  bj-nnord  16553  setindft  16560  bj-inf2vnlem2  16566  bj-inf2vnlem3  16567  bj-inf2vnlem4  16568  exmidsbthrlem  16626  triap  16633  tridceq  16660