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  806  pm4.72  829  pm2.18dc  857  con1dc  858  jadc  865  pm2.521dcALT  872  con1biimdc  875  condandc  883  pm5.18dc  885  pm2.68dc  896  syl3an2  1284  syl2an23an  1312  xor3dc  1407  alrimdh  1503  spsd  1562  a5i  1567  19.21h  1581  hbnt  1677  hbae  1742  sbiedh  1811  exdistrfor  1824  sbcof2  1834  ax11a2  1845  ax11v  1851  sb4  1856  hbsb4t  2042  exmoeudc  2119  euimmo  2123  mopick  2134  r19.37  2660  spcimgft  2856  spcimegft  2858  rr19.28v  2920  mob2  2960  euind  2967  reuind  2985  sbeqalb  3062  triun  4171  csbexga  4188  copsexg  4306  trssord  4445  trsuc  4487  trsucss  4488  abnexg  4511  ralxfrd  4527  rexxfrd  4528  ralxfrALT  4532  sucprcreg  4615  nlimsucg  4632  tfis  4649  relssres  5016  issref  5084  dmsnopg  5173  dfco2a  5202  imadif  5373  fvelima  5653  mptfvex  5688  fvmptdf  5690  fvmptf  5695  funfvima2  5840  funfvima3  5841  foco2  5845  isores3  5907  oprabid  5999  ovmpt4g  6091  ovmpos  6092  ov2gf  6093  ovmpodf  6100  suppssfv  6177  suppssov1  6178  fo2ndf  6336  rntpos  6366  tposf2  6377  nnmordi  6625  nnmord  6626  nnaordex  6637  ectocld  6711  qsel  6722  mapsn  6800  f1oeng  6871  mapen  6968  nneneq  6979  findcard2  7012  findcard2s  7013  ac6sfi  7021  fiintim  7054  sbthlem1  7085  pr2ne  7326  ltbtwnnqq  7563  prnmaddl  7638  genpcdl  7667  genpcuu  7668  ltaddpr  7745  lteupri  7765  recexprlemss1l  7783  recexprlemss1u  7784  cauappcvgprlemdisj  7799  lttrsr  7910  recexgt0sr  7921  mulgt0sr  7926  axprecex  8028  rereceu  8037  addlsub  8477  recexap  8761  0mnnnnn0  9362  prime  9507  zeo  9513  fnn0ind  9524  zindd  9526  btwnz  9527  lbzbi  9772  addmodlteq  10580  facwordi  10922  seq3coll  11024  pfxccatin12lem2a  11218  qdenre  11628  climcau  11773  serf0  11778  zsumdc  11810  fsum2dlemstep  11860  fsum2d  11861  fsumabs  11891  fsumiun  11903  zproddc  12005  fprod2dlemstep  12048  fprod2d  12049  odd2np1  12299  ndvdssub  12356  bitsinv1lem  12387  dfgcd2  12450  nprm  12560  rpexp  12590  pc2dvds  12768  pcfac  12788  4sqlem12  12840  4sqlem17  12845  divsfval  13275  mulgaddcom  13597  mulginvcom  13598  ringinvnz1ne0  13926  lmss  14833  lmtopcnp  14837  txcn  14862  txlm  14866  xmettri2  14948  blin2  15019  metcnp3  15098  limcresi  15253  dvmptfsum  15312  logbgcd1irr  15554  lgsdir2lem2  15621  lgsne0  15630  2lgsoddprm  15705  2sqlem6  15712  2sqlem10  15717  uhgr0vb  15795  bj-stim  15882  bj-stan  15883  bj-stand  15884  bj-stal  15885  bj-sbimedh  15907  bj-vtoclgft  15911  elabgft1  15914  elabgf2  15916