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  447  con2d  619  con3d  626  expi  633  pm3.37  684  pm5.21ndd  700  pm2.37  800  pm2.81  806  dcim  836  condcOLD  849  con4biddc  852  pm2.54dc  886  pm4.79dc  898  pm2.85dc  900  pm3.12dc  953  dn1dc  955  3jao  1296  xoranor  1372  syl6an  1427  syl10  1428  hbald  1484  ax12  1505  hbimd  1566  nfal  1569  19.21ht  1574  19.30dc  1620  19.23t  1670  hbexd  1687  spimth  1728  spimed  1733  cbv2h  1741  cbv2w  1743  equvini  1751  sbiedh  1780  sbcof2  1803  aev  1805  sb3  1824  hbsb2  1829  sbequilem  1831  sbft  1841  sbi1v  1884  cbvexdh  1919  nf5-1  2017  mo23  2060  moexexdc  2103  euexex  2104  exists2  2116  dvelimdc  2333  rsp2  2520  rgen2a  2524  spcimgft  2806  spcimegft  2808  eueq3dc  2904  moeq3dc  2906  reu6  2919  ssddif  3361  reupick2  3413  sssnm  3741  prneimg  3761  dfiun2g  3905  exmidsssnc  4189  exmidundifim  4193  opth1  4221  copsexg  4229  opelopabt  4247  issod  4304  sowlin  4305  suctr  4406  reusv3i  4444  ralxfrALT  4452  ssorduni  4471  onintonm  4501  regexmidlem1  4517  nlimsucg  4550  0elnn  4603  issref  4993  iotaval  5171  fun11iun  5463  brprcneu  5489  fvssunirng  5511  relfvssunirn  5512  fv3  5519  ndmfvg  5527  ssimaex  5557  fvopab3ig  5570  dff4im  5642  ffnfv  5654  fconstfvm  5714  f1mpt  5750  oprabid  5885  mpoeq123  5912  f1o2ndf1  6207  brtposg  6233  rntpos  6236  dftpos4  6242  smores2  6273  tfri3  6346  rdgss  6362  nntri3or  6472  nndifsnid  6486  nnawordex  6508  eroveu  6604  map0g  6666  fundmen  6784  nneneq  6835  fiintim  6906  snon0  6913  fnfi  6914  infnlbti  7003  exmidonfinlem  7170  exmidontri2or  7220  addclpi  7289  enq0tr  7396  genprndl  7483  genprndu  7484  genpdisj  7485  addlocprlem  7497  nqprloc  7507  recexprlemss1l  7597  recexprlemss1u  7598  suplocexprlemss  7677  elrealeu  7791  ltleletr  8001  negf1o  8301  zletric  9256  zlelttric  9257  zltnle  9258  zmulcl  9265  zdcle  9288  zdclt  9289  zeo  9317  uz11  9509  indstr  9552  eqreznegel  9573  negm  9574  lbzbi  9575  fzdcel  9996  fzm1  10056  qletric  10200  qlelttric  10201  qltnle  10202  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  qsqeqor  10586  rennim  10966  maxleast  11177  negfi  11191  fsum3cvg  11341  fproddccvg  11535  prodmodc  11541  ndvdssub  11889  algcvgblem  12003  algcvga  12005  isprm3  12072  oddprmdvds  12306  4sqlem2  12341  epttop  12884  cnptoprest  13033  txcnp  13065  metequiv2  13290  cnlimcim  13434  bj-hbalt  13798  bj-intabssel1  13825  decidin  13832  sumdc2  13834  bj-charfunr  13845  bj-axemptylem  13927  bj-nnen2lp  13989  bj-nnord  13993  setindft  14000  bj-inf2vnlem2  14006  bj-inf2vnlem3  14007  bj-inf2vnlem4  14008  exmidsbthrlem  14054  triap  14061  tridceq  14088