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  654  pm2.36  812  pm4.72  835  pm2.18dc  863  con1dc  864  jadc  871  pm2.521dcALT  878  con1biimdc  881  condandc  889  pm5.18dc  891  pm2.68dc  902  syl3an2  1308  syl2an23an  1336  xor3dc  1432  alrimdh  1528  spsd  1587  a5i  1592  19.21h  1606  hbnt  1701  hbae  1766  sbiedh  1836  exdistrfor  1849  sbcof2  1859  ax11a2  1870  ax11v  1876  sb4  1881  hbsb4t  2067  exmoeudc  2144  euimmo  2148  mopick  2159  r19.37  2695  spcimgft  2893  spcimegft  2895  rr19.28v  2957  mob2  2997  euind  3004  reuind  3022  sbeqalb  3099  triun  4221  csbexga  4238  copsexg  4360  trssord  4501  trsuc  4543  trsucss  4544  abnexg  4567  ralxfrd  4583  rexxfrd  4584  ralxfrALT  4588  sucprcreg  4671  nlimsucg  4688  tfis  4705  relssres  5076  issref  5145  dmsnopg  5234  dfco2a  5263  imadif  5436  fvelima  5728  mptfvex  5763  fvmptdf  5765  fvmptf  5770  funfvima2  5919  funfvima3  5920  foco2  5926  isores3  5988  oprabid  6082  ovmpt4g  6176  ovmpos  6177  ov2gf  6178  ovmpodf  6185  suppssov1  6263  fo2ndf  6423  suppssfvg  6463  rntpos  6488  tposf2  6499  nnmordi  6749  nnmord  6750  nnaordex  6761  ectocld  6835  qsel  6846  mapsn  6925  f1oeng  6996  mapen  7099  nneneq  7111  findcard2  7146  findcard2s  7147  ac6sfi  7155  fiintim  7191  sbthlem1  7227  pr2ne  7489  ltbtwnnqq  7730  prnmaddl  7805  genpcdl  7834  genpcuu  7835  ltaddpr  7912  lteupri  7932  recexprlemss1l  7950  recexprlemss1u  7951  cauappcvgprlemdisj  7966  lttrsr  8077  recexgt0sr  8088  mulgt0sr  8093  axprecex  8195  rereceu  8204  addlsub  8643  recexap  8927  0mnnnnn0  9528  prime  9677  zeo  9683  fnn0ind  9694  zindd  9696  btwnz  9697  lbzbi  9948  addmodlteq  10760  facwordi  11102  seq3coll  11214  ccatalpha  11301  pfxccatin12lem2a  11419  qdenre  11887  climcau  12032  serf0  12037  zsumdc  12070  fsum2dlemstep  12120  fsum2d  12121  fsumabs  12151  fsumiun  12163  zproddc  12265  fprod2dlemstep  12308  fprod2d  12309  odd2np1  12559  ndvdssub  12616  bitsinv1lem  12647  dfgcd2  12710  nprm  12820  rpexp  12850  pc2dvds  13028  pcfac  13048  4sqlem12  13100  4sqlem17  13105  divsfval  13541  mulgaddcom  13863  mulginvcom  13864  ringinvnz1ne0  14193  lmss  15111  lmtopcnp  15115  txcn  15140  txlm  15144  xmettri2  15226  blin2  15297  metcnp3  15376  limcresi  15531  dvmptfsum  15590  logbgcd1irr  15832  lgsdir2lem2  15902  lgsne0  15911  2lgsoddprm  15986  2sqlem6  15993  2sqlem10  15998  uhgr0vb  16079  wlk1walkdom  16354  wlkv0  16364  wlklenvclwlk  16368  bj-stim  16518  bj-stan  16519  bj-stand  16520  bj-stal  16521  bj-sbimedh  16543  bj-vtoclgft  16547  elabgft1  16550  elabgf2  16552