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  8710  zletric  9692  zlelttric  9693  zltnle  9694  zmulcl  9702  zdcle  9725  zdclt  9726  zeo  9755  uz11  9954  indstr  10002  eqreznegel  10023  negm  10024  lbzbi  10025  fzdcel  10454  fzm1  10517  qletric  10686  qlelttric  10687  qltnle  10688  qdclt  10690  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  qsqeqor  11100  swrdccatin2d  11530  rennim  11782  maxleast  11994  negfi  12009  fsum3cvg  12161  fproddccvg  12355  prodmodc  12361  ndvdssub  12713  bitsinv1lem  12744  algcvgblem  12843  algcvga  12845  isprm3  12912  oddprmdvds  13153  4sqlem2  13188  ballotfilemfc0  13281  ballotfilemfcc  13282  imasaddfnlemg  13684  subrngintm  14569  subrgintm  14600  lmodfopnelem1  14710  islssm  14743  lspsneq0  14812  islidlm  14865  epttop  15240  cnptoprest  15389  txcnp  15421  metequiv2  15646  cnlimcim  15821  ppiublem1  16192  umgrclwwlkge2  16741  bj-hbalt  16889  bj-intabssel1  16916  decidin  16923  sumdc2  16925  bj-charfunr  16934  bj-axemptylem  17016  bj-nnen2lp  17078  bj-nnord  17082  setindft  17089  bj-inf2vnlem2  17095  bj-inf2vnlem3  17096  bj-inf2vnlem4  17097  exmidsbthrlem  17165  triap  17176  tridceq  17204