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  1283  xoranor  1359  syl6an  1414  syl10  1415  hbald  1471  ax12  1492  hbimd  1553  nfal  1556  19.21ht  1561  19.30dc  1607  19.23t  1657  hbexd  1674  spimth  1715  spimed  1720  cbv2h  1728  cbv2w  1730  equvini  1738  sbiedh  1767  sbcof2  1790  aev  1792  sb3  1811  hbsb2  1816  sbequilem  1818  sbft  1828  sbi1v  1871  cbvexdh  1906  nf5-1  2004  mo23  2047  moexexdc  2090  euexex  2091  exists2  2103  dvelimdc  2320  rsp2  2507  rgen2a  2511  spcimgft  2788  spcimegft  2790  eueq3dc  2886  moeq3dc  2888  reu6  2901  ssddif  3342  reupick2  3394  sssnm  3719  prneimg  3739  dfiun2g  3883  exmidsssnc  4167  exmidundifim  4171  opth1  4199  copsexg  4207  opelopabt  4225  issod  4282  sowlin  4283  suctr  4384  reusv3i  4422  ralxfrALT  4430  ssorduni  4449  onintonm  4479  regexmidlem1  4495  nlimsucg  4528  0elnn  4581  issref  4971  iotaval  5149  fun11iun  5438  brprcneu  5464  fvssunirng  5486  relfvssunirn  5487  fv3  5494  ndmfvg  5502  ssimaex  5532  fvopab3ig  5545  dff4im  5616  ffnfv  5628  fconstfvm  5688  f1mpt  5724  oprabid  5856  mpoeq123  5883  f1o2ndf1  6178  brtposg  6204  rntpos  6207  dftpos4  6213  smores2  6244  tfri3  6317  rdgss  6333  nntri3or  6443  nndifsnid  6457  nnawordex  6478  eroveu  6574  map0g  6636  fundmen  6754  nneneq  6805  fiintim  6876  snon0  6883  fnfi  6884  infnlbti  6973  exmidonfinlem  7131  exmidontri2or  7181  addclpi  7250  enq0tr  7357  genprndl  7444  genprndu  7445  genpdisj  7446  addlocprlem  7458  nqprloc  7468  recexprlemss1l  7558  recexprlemss1u  7559  suplocexprlemss  7638  elrealeu  7752  ltleletr  7962  negf1o  8262  zletric  9217  zlelttric  9218  zltnle  9219  zmulcl  9226  zdcle  9246  zdclt  9247  zeo  9275  uz11  9467  indstr  9510  eqreznegel  9530  negm  9531  lbzbi  9532  fzdcel  9949  fzm1  10009  qletric  10153  qlelttric  10154  qltnle  10155  frecuzrdgtcl  10321  frecuzrdgfunlem  10328  rennim  10914  maxleast  11125  negfi  11139  fsum3cvg  11287  fproddccvg  11481  prodmodc  11487  ndvdssub  11834  algcvgblem  11942  algcvga  11944  isprm3  12011  epttop  12586  cnptoprest  12735  txcnp  12767  metequiv2  12992  cnlimcim  13136  bj-hbalt  13434  bj-intabssel1  13461  decidin  13468  sumdc2  13470  bj-charfunr  13482  bj-axemptylem  13564  bj-nnen2lp  13626  bj-nnord  13630  setindft  13637  bj-inf2vnlem2  13643  bj-inf2vnlem3  13644  bj-inf2vnlem4  13645  exmidsbthrlem  13690  triap  13697  tridceq  13724