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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  454  con2d  633  con3d  640  expi  647  pm3.37  700  pm5.21ndd  717  pm2.37  817  pm2.81  823  dcim  853  condcOLD  866  con4biddc  869  pm2.54dc  903  pm4.79dc  915  pm2.85dc  917  pm3.12dc  971  dn1dc  973  3jao  1342  xoranor  1426  syl6an  1483  syl10  1484  hbald  1544  ax12  1565  hbimd  1626  nfal  1629  19.21ht  1634  19.30dc  1680  19.23t  1729  hbexd  1746  spimth  1788  spimed  1793  cbv2h  1801  cbv2w  1803  equvini  1811  sbiedh  1840  sbcof2  1863  aev  1865  sb3  1884  hbsb2  1889  sbequilem  1891  sbft  1901  sbi1v  1946  cbvexdh  1982  nf5-1  2084  mo23  2128  moexexdc  2171  euexex  2172  exists2  2184  dvelimdc  2413  rsp2  2600  rgen2a  2604  spcimgft  2901  spcimegft  2903  eueq3dc  3000  moeq3dc  3002  reu6  3015  ssddif  3465  reupick2  3519  ifnebibdc  3686  sssnm  3879  prneimg  3899  dfiun2g  4044  exmidsssnc  4340  exmidundifim  4344  opth1  4376  copsexg  4384  opelopabt  4404  issod  4464  sowlin  4465  suctr  4566  reusv3i  4605  ralxfrALT  4613  ssorduni  4634  onintonm  4664  regexmidlem1  4680  nlimsucg  4713  0elnn  4766  ssrelrn  4972  issref  5170  iotaval  5349  fun11iun  5660  brprcneu  5688  fvssunirng  5710  relfvssunirn  5711  fv3  5718  ndmfvg  5726  ssimaex  5764  fvopab3ig  5779  dff4im  5854  ffnfv  5866  fconstfvm  5933  f1mpt  5977  oprabid  6117  mpoeq123  6147  f1o2ndf1  6464  brtposg  6525  rntpos  6528  dftpos4  6534  smores2  6565  tfri3  6638  rdgss  6654  nntri3or  6766  nndifsnid  6780  nnawordex  6802  eroveu  6900  map0g  6969  fundmen  7094  nneneq  7158  fiintim  7238  snon0  7249  fnfi  7250  infnlbti  7366  exmidonfinlem  7545  exmidontri2or  7602  addclpi  7694  enq0tr  7801  genprndl  7888  genprndu  7889  genpdisj  7890  addlocprlem  7902  nqprloc  7912  recexprlemss1l  8002  recexprlemss1u  8003  suplocexprlemss  8082  elrealeu  8196  ltleletr  8407  negf1o  8709  zletric  9688  zlelttric  9689  zltnle  9690  zmulcl  9698  zdcle  9721  zdclt  9722  zeo  9751  uz11  9945  indstr  9993  eqreznegel  10014  negm  10015  lbzbi  10016  fzdcel  10444  fzm1  10507  qletric  10676  qlelttric  10677  qltnle  10678  qdclt  10680  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  qsqeqor  11087  swrdccatin2d  11516  rennim  11768  maxleast  11979  negfi  11994  fsum3cvg  12145  fproddccvg  12339  prodmodc  12345  ndvdssub  12697  bitsinv1lem  12728  algcvgblem  12827  algcvga  12829  isprm3  12896  oddprmdvds  13133  4sqlem2  13168  ballotfilemfc0  13232  ballotfilemfcc  13233  imasaddfnlemg  13635  subrngintm  14520  subrgintm  14551  lmodfopnelem1  14661  islssm  14694  lspsneq0  14763  islidlm  14816  epttop  15191  cnptoprest  15340  txcnp  15372  metequiv2  15597  cnlimcim  15772  umgrclwwlkge2  16643  bj-hbalt  16791  bj-intabssel1  16818  decidin  16825  sumdc2  16827  bj-charfunr  16836  bj-axemptylem  16918  bj-nnen2lp  16980  bj-nnord  16984  setindft  16991  bj-inf2vnlem2  16997  bj-inf2vnlem3  16998  bj-inf2vnlem4  16999  exmidsbthrlem  17067  triap  17078  tridceq  17106