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  625  con3d  632  expi  639  pm3.37  690  pm5.21ndd  706  pm2.37  806  pm2.81  812  dcim  842  condcOLD  855  con4biddc  858  pm2.54dc  892  pm4.79dc  904  pm2.85dc  906  pm3.12dc  960  dn1dc  962  3jao  1313  xoranor  1396  syl6an  1453  syl10  1454  hbald  1513  ax12  1534  hbimd  1595  nfal  1598  19.21ht  1603  19.30dc  1649  19.23t  1699  hbexd  1716  spimth  1757  spimed  1762  cbv2h  1770  cbv2w  1772  equvini  1780  sbiedh  1809  sbcof2  1832  aev  1834  sb3  1853  hbsb2  1858  sbequilem  1860  sbft  1870  sbi1v  1914  cbvexdh  1949  nf5-1  2051  mo23  2094  moexexdc  2137  euexex  2138  exists2  2150  dvelimdc  2368  rsp2  2555  rgen2a  2559  spcimgft  2848  spcimegft  2850  eueq3dc  2946  moeq3dc  2948  reu6  2961  ssddif  3406  reupick2  3458  ifnebibdc  3614  sssnm  3794  prneimg  3814  dfiun2g  3958  exmidsssnc  4246  exmidundifim  4250  opth1  4279  copsexg  4287  opelopabt  4306  issod  4364  sowlin  4365  suctr  4466  reusv3i  4504  ralxfrALT  4512  ssorduni  4533  onintonm  4563  regexmidlem1  4579  nlimsucg  4612  0elnn  4665  issref  5062  iotaval  5240  fun11iun  5537  brprcneu  5563  fvssunirng  5585  relfvssunirn  5586  fv3  5593  ndmfvg  5601  ssimaex  5634  fvopab3ig  5647  dff4im  5720  ffnfv  5732  fconstfvm  5792  f1mpt  5830  oprabid  5966  mpoeq123  5994  f1o2ndf1  6304  brtposg  6330  rntpos  6333  dftpos4  6339  smores2  6370  tfri3  6443  rdgss  6459  nntri3or  6569  nndifsnid  6583  nnawordex  6605  eroveu  6703  map0g  6765  fundmen  6883  nneneq  6936  fiintim  7010  snon0  7019  fnfi  7020  infnlbti  7110  exmidonfinlem  7283  exmidontri2or  7337  addclpi  7422  enq0tr  7529  genprndl  7616  genprndu  7617  genpdisj  7618  addlocprlem  7630  nqprloc  7640  recexprlemss1l  7730  recexprlemss1u  7731  suplocexprlemss  7810  elrealeu  7924  ltleletr  8136  negf1o  8436  zletric  9398  zlelttric  9399  zltnle  9400  zmulcl  9408  zdcle  9431  zdclt  9432  zeo  9460  uz11  9653  indstr  9696  eqreznegel  9717  negm  9718  lbzbi  9719  fzdcel  10144  fzm1  10204  qletric  10365  qlelttric  10366  qltnle  10367  qdclt  10369  frecuzrdgtcl  10538  frecuzrdgfunlem  10545  qsqeqor  10776  rennim  11232  maxleast  11443  negfi  11458  fsum3cvg  11608  fproddccvg  11802  prodmodc  11808  ndvdssub  12160  bitsinv1lem  12191  algcvgblem  12290  algcvga  12292  isprm3  12359  oddprmdvds  12596  4sqlem2  12631  imasaddfnlemg  13064  subrngintm  13892  subrgintm  13923  lmodfopnelem1  14004  islssm  14037  lspsneq0  14106  islidlm  14159  epttop  14480  cnptoprest  14629  txcnp  14661  metequiv2  14886  cnlimcim  15061  bj-hbalt  15563  bj-intabssel1  15590  decidin  15597  sumdc2  15599  bj-charfunr  15610  bj-axemptylem  15692  bj-nnen2lp  15754  bj-nnord  15758  setindft  15765  bj-inf2vnlem2  15771  bj-inf2vnlem3  15772  bj-inf2vnlem4  15773  exmidsbthrlem  15825  triap  15832  tridceq  15859