Theorem syl5 32

Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

Ref	Expression
syl5.1	|- ( ph -> ps )
syl5.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 |- ( ph -> ps )
2		syl5.2	. . 3 |- ( ch -> ( ps -> th ) )
3	1, 2	syl5com 29	. 2 |- ( ph -> ( ch -> th ) )
4	3	com12 30	1 |- ( ch -> ( ph -> 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  syl2im  38  imim12i  59  pm2.86d  100  biimtrid  152  biimtrrid  153  imbitrid  154  adantld  278  adantrd  279  impel  280  mpan9  281  nsyli  650  pm2.36  805  pm4.72  828  pm2.18dc  856  con1dc  857  jadc  864  pm2.521dcALT  871  con1biimdc  874  condandc  882  pm5.18dc  884  pm2.68dc  895  syl3an2  1283  syl2an23an  1310  xor3dc  1398  alrimdh  1493  spsd  1552  a5i  1557  19.21h  1571  hbnt  1667  hbae  1732  sbiedh  1801  exdistrfor  1814  sbcof2  1824  ax11a2  1835  ax11v  1841  sb4  1846  hbsb4t  2032  exmoeudc  2108  euimmo  2112  mopick  2123  r19.37  2649  spcimgft  2840  spcimegft  2842  rr19.28v  2904  mob2  2944  euind  2951  reuind  2969  sbeqalb  3046  triun  4145  csbexga  4162  copsexg  4278  trssord  4416  trsuc  4458  trsucss  4459  abnexg  4482  ralxfrd  4498  rexxfrd  4499  ralxfrALT  4503  sucprcreg  4586  nlimsucg  4603  tfis  4620  relssres  4985  issref  5053  dmsnopg  5142  dfco2a  5171  imadif  5339  fvelima  5615  mptfvex  5650  fvmptdf  5652  fvmptf  5657  funfvima2  5798  funfvima3  5799  foco2  5803  isores3  5865  oprabid  5957  ovmpt4g  6049  ovmpos  6050  ov2gf  6051  ovmpodf  6058  suppssfv  6135  suppssov1  6136  fo2ndf  6294  rntpos  6324  tposf2  6335  nnmordi  6583  nnmord  6584  nnaordex  6595  ectocld  6669  qsel  6680  mapsn  6758  f1oeng  6825  mapen  6916  nneneq  6927  findcard2  6959  findcard2s  6960  ac6sfi  6968  fiintim  7001  sbthlem1  7032  pr2ne  7271  ltbtwnnqq  7499  prnmaddl  7574  genpcdl  7603  genpcuu  7604  ltaddpr  7681  lteupri  7701  recexprlemss1l  7719  recexprlemss1u  7720  cauappcvgprlemdisj  7735  lttrsr  7846  recexgt0sr  7857  mulgt0sr  7862  axprecex  7964  rereceu  7973  addlsub  8413  recexap  8697  0mnnnnn0  9298  prime  9442  zeo  9448  fnn0ind  9459  zindd  9461  btwnz  9462  lbzbi  9707  addmodlteq  10507  facwordi  10849  seq3coll  10951  qdenre  11384  climcau  11529  serf0  11534  zsumdc  11566  fsum2dlemstep  11616  fsum2d  11617  fsumabs  11647  fsumiun  11659  zproddc  11761  fprod2dlemstep  11804  fprod2d  11805  odd2np1  12055  ndvdssub  12112  bitsinv1lem  12143  dfgcd2  12206  nprm  12316  rpexp  12346  pc2dvds  12524  pcfac  12544  4sqlem12  12596  4sqlem17  12601  divsfval  13030  mulgaddcom  13352  mulginvcom  13353  ringinvnz1ne0  13681  lmss  14566  lmtopcnp  14570  txcn  14595  txlm  14599  xmettri2  14681  blin2  14752  metcnp3  14831  limcresi  14986  dvmptfsum  15045  logbgcd1irr  15287  lgsdir2lem2  15354  lgsne0  15363  2lgsoddprm  15438  2sqlem6  15445  2sqlem10  15450  bj-stim  15476  bj-stan  15477  bj-stand  15478  bj-stal  15479  bj-sbimedh  15501  bj-vtoclgft  15505  elabgft1  15508  elabgf2  15510