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  114  syl6ib  160  syl6ibr  161  syl6bi  162  syl6bir  163  pm5.32d  446  con2d  614  con3d  621  expi  628  pm3.37  679  pm5.21ndd  695  pm2.37  795  pm2.81  801  dcim  827  condcOLD  840  con4biddc  843  pm2.54dc  877  pm4.79dc  889  pm2.85dc  891  pm3.12dc  943  dn1dc  945  3jao  1280  xoranor  1356  syl6an  1411  syl10  1412  hbald  1468  ax-12  1490  hbimd  1553  19.21ht  1561  19.30dc  1607  19.23t  1656  hbexd  1673  spimth  1714  spimed  1719  cbv2h  1725  equvini  1732  sbiedh  1761  sbcof2  1783  aev  1785  sb3  1804  hbsb2  1809  sbequilem  1811  sbft  1821  sbi1v  1864  cbvexdh  1899  mo23  2041  moexexdc  2084  euexex  2085  exists2  2097  dvelimdc  2302  rsp2  2485  rgen2a  2489  spcimgft  2765  spcimegft  2767  eueq3dc  2862  moeq3dc  2864  reu6  2877  ssddif  3315  reupick2  3367  sssnm  3689  prneimg  3709  dfiun2g  3853  exmidsssnc  4134  exmidundifim  4138  opth1  4166  copsexg  4174  opelopabt  4192  issod  4249  sowlin  4250  suctr  4351  reusv3i  4388  ralxfrALT  4396  ssorduni  4411  onintonm  4441  regexmidlem1  4456  nlimsucg  4489  0elnn  4540  issref  4929  iotaval  5107  fun11iun  5396  brprcneu  5422  fvssunirng  5444  relfvssunirn  5445  fv3  5452  ndmfvg  5460  ssimaex  5490  fvopab3ig  5503  dff4im  5574  ffnfv  5586  fconstfvm  5646  f1mpt  5680  oprabid  5811  mpoeq123  5838  f1o2ndf1  6133  brtposg  6159  rntpos  6162  dftpos4  6168  smores2  6199  tfri3  6272  rdgss  6288  nntri3or  6397  nndifsnid  6411  nnawordex  6432  eroveu  6528  map0g  6590  fundmen  6708  nneneq  6759  fiintim  6825  snon0  6832  fnfi  6833  infnlbti  6921  exmidonfinlem  7066  addclpi  7159  enq0tr  7266  genprndl  7353  genprndu  7354  genpdisj  7355  addlocprlem  7367  nqprloc  7377  recexprlemss1l  7467  recexprlemss1u  7468  suplocexprlemss  7547  elrealeu  7661  ltleletr  7870  negf1o  8168  zletric  9122  zlelttric  9123  zltnle  9124  zmulcl  9131  zdcle  9151  zdclt  9152  zeo  9180  uz11  9372  indstr  9415  eqreznegel  9433  negm  9434  lbzbi  9435  fzdcel  9851  fzm1  9911  qletric  10052  qlelttric  10053  qltnle  10054  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  rennim  10806  maxleast  11017  negfi  11031  fsum3cvg  11179  fproddccvg  11373  prodmodc  11379  ndvdssub  11663  algcvgblem  11766  algcvga  11768  isprm3  11835  epttop  12298  cnptoprest  12447  txcnp  12479  metequiv2  12704  cnlimcim  12848  bj-hbalt  13141  bj-intabssel1  13168  decidin  13175  sumdc2  13177  bj-axemptylem  13261  bj-nnen2lp  13323  bj-nnord  13327  setindft  13334  bj-inf2vnlem2  13340  bj-inf2vnlem3  13341  bj-inf2vnlem4  13342  exmidsbthrlem  13392  triap  13399