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  454  con2d  633  con3d  640  expi  647  pm3.37  700  pm5.21ndd  717  pm2.37  817  pm2.81  823  dcim  853  condcOLD  866  con4biddc  869  pm2.54dc  903  pm4.79dc  915  pm2.85dc  917  pm3.12dc  971  dn1dc  973  3jao  1342  xoranor  1426  syl6an  1483  syl10  1484  hbald  1544  ax12  1565  hbimd  1626  nfal  1629  19.21ht  1634  19.30dc  1680  19.23t  1729  hbexd  1746  spimth  1788  spimed  1793  cbv2h  1801  cbv2w  1803  equvini  1811  sbiedh  1840  sbcof2  1863  aev  1865  sb3  1884  hbsb2  1889  sbequilem  1891  sbft  1901  sbi1v  1946  cbvexdh  1982  nf5-1  2084  mo23  2128  moexexdc  2171  euexex  2172  exists2  2184  dvelimdc  2413  rsp2  2600  rgen2a  2604  spcimgft  2901  spcimegft  2903  eueq3dc  3000  moeq3dc  3002  reu6  3015  ssddif  3465  reupick2  3519  ifnebibdc  3683  sssnm  3874  prneimg  3894  dfiun2g  4039  exmidsssnc  4335  exmidundifim  4339  opth1  4371  copsexg  4379  opelopabt  4399  issod  4459  sowlin  4460  suctr  4561  reusv3i  4600  ralxfrALT  4608  ssorduni  4629  onintonm  4659  regexmidlem1  4675  nlimsucg  4708  0elnn  4761  ssrelrn  4967  issref  5165  iotaval  5344  fun11iun  5655  brprcneu  5683  fvssunirng  5705  relfvssunirn  5706  fv3  5713  ndmfvg  5721  ssimaex  5758  fvopab3ig  5773  dff4im  5845  ffnfv  5857  fconstfvm  5924  f1mpt  5967  oprabid  6107  mpoeq123  6137  f1o2ndf1  6454  brtposg  6515  rntpos  6518  dftpos4  6524  smores2  6555  tfri3  6628  rdgss  6644  nntri3or  6756  nndifsnid  6770  nnawordex  6792  eroveu  6890  map0g  6959  fundmen  7084  nneneq  7148  fiintim  7228  snon0  7239  fnfi  7240  infnlbti  7356  exmidonfinlem  7535  exmidontri2or  7592  addclpi  7684  enq0tr  7791  genprndl  7878  genprndu  7879  genpdisj  7880  addlocprlem  7892  nqprloc  7902  recexprlemss1l  7992  recexprlemss1u  7993  suplocexprlemss  8072  elrealeu  8186  ltleletr  8397  negf1o  8699  zletric  9667  zlelttric  9668  zltnle  9669  zmulcl  9677  zdcle  9700  zdclt  9701  zeo  9730  uz11  9924  indstr  9972  eqreznegel  9993  negm  9994  lbzbi  9995  fzdcel  10423  fzm1  10485  qletric  10654  qlelttric  10655  qltnle  10656  qdclt  10658  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  qsqeqor  11065  swrdccatin2d  11494  rennim  11746  maxleast  11957  negfi  11972  fsum3cvg  12123  fproddccvg  12317  prodmodc  12323  ndvdssub  12675  bitsinv1lem  12706  algcvgblem  12805  algcvga  12807  isprm3  12874  oddprmdvds  13111  4sqlem2  13146  ballotfilemfc0  13210  ballotfilemfcc  13211  imasaddfnlemg  13612  subrngintm  14493  subrgintm  14524  lmodfopnelem1  14633  islssm  14666  lspsneq0  14735  islidlm  14788  epttop  15114  cnptoprest  15263  txcnp  15295  metequiv2  15520  cnlimcim  15695  umgrclwwlkge2  16557  bj-hbalt  16705  bj-intabssel1  16732  decidin  16739  sumdc2  16741  bj-charfunr  16750  bj-axemptylem  16832  bj-nnen2lp  16894  bj-nnord  16898  setindft  16905  bj-inf2vnlem2  16911  bj-inf2vnlem3  16912  bj-inf2vnlem4  16913  exmidsbthrlem  16972  triap  16983  tridceq  17011