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  696  pm5.21ndd  713  pm2.37  813  pm2.81  819  dcim  849  condcOLD  862  con4biddc  865  pm2.54dc  899  pm4.79dc  911  pm2.85dc  913  pm3.12dc  967  dn1dc  969  3jao  1338  xoranor  1422  syl6an  1479  syl10  1480  hbald  1540  ax12  1561  hbimd  1622  nfal  1625  19.21ht  1630  19.30dc  1676  19.23t  1725  hbexd  1742  spimth  1784  spimed  1789  cbv2h  1797  cbv2w  1799  equvini  1807  sbiedh  1836  sbcof2  1859  aev  1861  sb3  1880  hbsb2  1885  sbequilem  1887  sbft  1897  sbi1v  1942  cbvexdh  1978  nf5-1  2080  mo23  2124  moexexdc  2167  euexex  2168  exists2  2180  dvelimdc  2407  rsp2  2594  rgen2a  2598  spcimgft  2895  spcimegft  2897  eueq3dc  2994  moeq3dc  2996  reu6  3009  ssddif  3459  reupick2  3511  ifnebibdc  3672  sssnm  3863  prneimg  3883  dfiun2g  4028  exmidsssnc  4321  exmidundifim  4325  opth1  4357  copsexg  4365  opelopabt  4385  issod  4445  sowlin  4446  suctr  4547  reusv3i  4585  ralxfrALT  4593  ssorduni  4614  onintonm  4644  regexmidlem1  4660  nlimsucg  4693  0elnn  4746  ssrelrn  4952  issref  5150  iotaval  5329  fun11iun  5640  brprcneu  5668  fvssunirng  5690  relfvssunirn  5691  fv3  5698  ndmfvg  5706  ssimaex  5743  fvopab3ig  5756  dff4im  5828  ffnfv  5840  fconstfvm  5907  f1mpt  5950  oprabid  6090  mpoeq123  6120  f1o2ndf1  6437  brtposg  6498  rntpos  6501  dftpos4  6507  smores2  6538  tfri3  6611  rdgss  6627  nntri3or  6739  nndifsnid  6753  nnawordex  6775  eroveu  6873  map0g  6935  fundmen  7060  nneneq  7124  fiintim  7204  snon0  7215  fnfi  7216  infnlbti  7330  exmidonfinlem  7509  exmidontri2or  7566  addclpi  7658  enq0tr  7765  genprndl  7852  genprndu  7853  genpdisj  7854  addlocprlem  7866  nqprloc  7876  recexprlemss1l  7966  recexprlemss1u  7967  suplocexprlemss  8046  elrealeu  8160  ltleletr  8371  negf1o  8672  zletric  9638  zlelttric  9639  zltnle  9640  zmulcl  9648  zdcle  9671  zdclt  9672  zeo  9701  uz11  9895  indstr  9943  eqreznegel  9964  negm  9965  lbzbi  9966  fzdcel  10394  fzm1  10456  qletric  10625  qlelttric  10626  qltnle  10627  qdclt  10629  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  qsqeqor  11036  swrdccatin2d  11461  rennim  11712  maxleast  11923  negfi  11938  fsum3cvg  12089  fproddccvg  12283  prodmodc  12289  ndvdssub  12641  bitsinv1lem  12672  algcvgblem  12771  algcvga  12773  isprm3  12840  oddprmdvds  13077  4sqlem2  13112  ballotfilemfc0  13176  ballotfilemfcc  13177  imasaddfnlemg  13578  subrngintm  14458  subrgintm  14489  lmodfopnelem1  14598  islssm  14631  lspsneq0  14700  islidlm  14753  epttop  15081  cnptoprest  15230  txcnp  15262  metequiv2  15487  cnlimcim  15662  umgrclwwlkge2  16523  bj-hbalt  16661  bj-intabssel1  16688  decidin  16695  sumdc2  16697  bj-charfunr  16706  bj-axemptylem  16788  bj-nnen2lp  16850  bj-nnord  16854  setindft  16861  bj-inf2vnlem2  16867  bj-inf2vnlem3  16868  bj-inf2vnlem4  16869  exmidsbthrlem  16928  triap  16939  tridceq  16967