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  1502  spsd  1561  a5i  1566  19.21h  1580  hbnt  1676  hbae  1741  sbiedh  1810  exdistrfor  1823  sbcof2  1833  ax11a2  1844  ax11v  1850  sb4  1855  hbsb4t  2041  exmoeudc  2117  euimmo  2121  mopick  2132  r19.37  2658  spcimgft  2849  spcimegft  2851  rr19.28v  2913  mob2  2953  euind  2960  reuind  2978  sbeqalb  3055  triun  4155  csbexga  4172  copsexg  4288  trssord  4427  trsuc  4469  trsucss  4470  abnexg  4493  ralxfrd  4509  rexxfrd  4510  ralxfrALT  4514  sucprcreg  4597  nlimsucg  4614  tfis  4631  relssres  4997  issref  5065  dmsnopg  5154  dfco2a  5183  imadif  5354  fvelima  5630  mptfvex  5665  fvmptdf  5667  fvmptf  5672  funfvima2  5817  funfvima3  5818  foco2  5822  isores3  5884  oprabid  5976  ovmpt4g  6068  ovmpos  6069  ov2gf  6070  ovmpodf  6077  suppssfv  6154  suppssov1  6155  fo2ndf  6313  rntpos  6343  tposf2  6354  nnmordi  6602  nnmord  6603  nnaordex  6614  ectocld  6688  qsel  6699  mapsn  6777  f1oeng  6848  mapen  6943  nneneq  6954  findcard2  6986  findcard2s  6987  ac6sfi  6995  fiintim  7028  sbthlem1  7059  pr2ne  7300  ltbtwnnqq  7528  prnmaddl  7603  genpcdl  7632  genpcuu  7633  ltaddpr  7710  lteupri  7730  recexprlemss1l  7748  recexprlemss1u  7749  cauappcvgprlemdisj  7764  lttrsr  7875  recexgt0sr  7886  mulgt0sr  7891  axprecex  7993  rereceu  8002  addlsub  8442  recexap  8726  0mnnnnn0  9327  prime  9472  zeo  9478  fnn0ind  9489  zindd  9491  btwnz  9492  lbzbi  9737  addmodlteq  10543  facwordi  10885  seq3coll  10987  qdenre  11513  climcau  11658  serf0  11663  zsumdc  11695  fsum2dlemstep  11745  fsum2d  11746  fsumabs  11776  fsumiun  11788  zproddc  11890  fprod2dlemstep  11933  fprod2d  11934  odd2np1  12184  ndvdssub  12241  bitsinv1lem  12272  dfgcd2  12335  nprm  12445  rpexp  12475  pc2dvds  12653  pcfac  12673  4sqlem12  12725  4sqlem17  12730  divsfval  13160  mulgaddcom  13482  mulginvcom  13483  ringinvnz1ne0  13811  lmss  14718  lmtopcnp  14722  txcn  14747  txlm  14751  xmettri2  14833  blin2  14904  metcnp3  14983  limcresi  15138  dvmptfsum  15197  logbgcd1irr  15439  lgsdir2lem2  15506  lgsne0  15515  2lgsoddprm  15590  2sqlem6  15597  2sqlem10  15602  bj-stim  15682  bj-stan  15683  bj-stand  15684  bj-stal  15685  bj-sbimedh  15707  bj-vtoclgft  15711  elabgft1  15714  elabgf2  15716