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  445  con2d  613  con3d  620  expi  627  pm3.37  678  pm5.21ndd  694  pm2.37  794  pm2.81  800  dcim  826  condcOLD  839  con4biddc  842  pm2.54dc  876  pm4.79dc  888  pm2.85dc  890  pm3.12dc  942  dn1dc  944  3jao  1279  xoranor  1355  syl6an  1410  syl10  1411  hbald  1467  ax-12  1489  hbimd  1552  19.21ht  1560  19.30dc  1606  19.23t  1655  hbexd  1672  spimth  1713  spimed  1718  cbv2h  1724  equvini  1731  sbiedh  1760  sbcof2  1782  aev  1784  sb3  1803  hbsb2  1808  sbequilem  1810  sbft  1820  sbi1v  1863  cbvexdh  1898  mo23  2040  moexexdc  2083  euexex  2084  exists2  2096  dvelimdc  2301  rsp2  2482  rgen2a  2486  spcimgft  2762  spcimegft  2764  eueq3dc  2858  moeq3dc  2860  reu6  2873  ssddif  3310  reupick2  3362  sssnm  3681  prneimg  3701  dfiun2g  3845  exmidsssnc  4126  exmidundifim  4130  opth1  4158  copsexg  4166  opelopabt  4184  issod  4241  sowlin  4242  suctr  4343  reusv3i  4380  ralxfrALT  4388  ssorduni  4403  onintonm  4433  regexmidlem1  4448  nlimsucg  4481  0elnn  4532  issref  4921  iotaval  5099  fun11iun  5388  brprcneu  5414  fvssunirng  5436  relfvssunirn  5437  fv3  5444  ndmfvg  5452  ssimaex  5482  fvopab3ig  5495  dff4im  5566  ffnfv  5578  fconstfvm  5638  f1mpt  5672  oprabid  5803  mpoeq123  5830  f1o2ndf1  6125  brtposg  6151  rntpos  6154  dftpos4  6160  smores2  6191  tfri3  6264  rdgss  6280  nntri3or  6389  nndifsnid  6403  nnawordex  6424  eroveu  6520  map0g  6582  fundmen  6700  nneneq  6751  fiintim  6817  snon0  6824  fnfi  6825  infnlbti  6913  exmidonfinlem  7049  addclpi  7135  enq0tr  7242  genprndl  7329  genprndu  7330  genpdisj  7331  addlocprlem  7343  nqprloc  7353  recexprlemss1l  7443  recexprlemss1u  7444  suplocexprlemss  7523  elrealeu  7637  ltleletr  7846  negf1o  8144  zletric  9098  zlelttric  9099  zltnle  9100  zmulcl  9107  zdcle  9127  zdclt  9128  zeo  9156  uz11  9348  indstr  9388  eqreznegel  9406  negm  9407  lbzbi  9408  fzdcel  9820  fzm1  9880  qletric  10021  qlelttric  10022  qltnle  10023  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  rennim  10774  maxleast  10985  negfi  10999  fsum3cvg  11147  fproddccvg  11341  prodmodc  11347  ndvdssub  11627  algcvgblem  11730  algcvga  11732  isprm3  11799  epttop  12259  cnptoprest  12408  txcnp  12440  metequiv2  12665  cnlimcim  12809  bj-hbalt  12970  bj-intabssel1  12997  decidin  13004  sumdc2  13006  bj-axemptylem  13090  bj-nnen2lp  13152  bj-nnord  13156  setindft  13163  bj-inf2vnlem2  13169  bj-inf2vnlem3  13170  bj-inf2vnlem4  13171  exmidsbthrlem  13217  triap  13224