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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  658  pm2.36  816  pm4.72  839  pm2.18dc  867  con1dc  868  jadc  875  pm2.521dcALT  882  con1biimdc  885  condandc  893  pm5.18dc  895  pm2.68dc  906  syl3an2  1312  syl2an23an  1340  xor3dc  1436  alrimdh  1532  spsd  1591  a5i  1596  19.21h  1610  hbnt  1705  hbae  1770  sbiedh  1840  exdistrfor  1853  sbcof2  1863  ax11a2  1874  ax11v  1880  sb4  1885  hbsb4t  2073  exmoeudc  2150  euimmo  2154  mopick  2165  r19.37  2703  spcimgft  2901  spcimegft  2903  rr19.28v  2966  mob2  3006  euind  3013  reuind  3031  sbeqalb  3108  triun  4242  csbexga  4261  copsexg  4384  trssord  4525  trsuc  4567  trsucss  4568  abnexg  4592  ralxfrd  4608  rexxfrd  4609  ralxfrALT  4613  sucprcreg  4696  nlimsucg  4713  tfis  4730  relssres  5101  issref  5170  dmsnopg  5259  dfco2a  5288  imadif  5461  fvelima  5754  mptfvex  5791  fvmptdf  5793  fvmptf  5798  funfvima2  5951  funfvima3  5952  foco2  5959  isores3  6021  oprabid  6117  ovmpt4g  6211  ovmpos  6212  ov2gf  6213  ovmpodf  6220  suppssov1  6299  fo2ndf  6463  suppssfvg  6503  rntpos  6528  tposf2  6539  nnmordi  6789  nnmord  6790  nnaordex  6801  ectocld  6875  qsel  6886  mapsn  6972  f1oeng  7043  mapen  7146  nneneq  7158  findcard2  7193  findcard2s  7194  ac6sfi  7202  fiintim  7238  sbthlem1  7274  pr2ne  7538  ltbtwnnqq  7782  prnmaddl  7857  genpcdl  7886  genpcuu  7887  ltaddpr  7964  lteupri  7984  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemdisj  8018  lttrsr  8129  recexgt0sr  8140  mulgt0sr  8145  axprecex  8247  rereceu  8256  addlsub  8696  recexap  8981  0mnnnnn0  9595  prime  9745  zeo  9751  fnn0ind  9762  zindd  9764  btwnz  9765  lbzbi  10016  addmodlteq  10835  facwordi  11178  seq3coll  11294  ccatalpha  11381  pfxccatin12lem2a  11499  qdenre  11968  climcau  12113  serf0  12118  zsumdc  12151  fsum2dlemstep  12201  fsum2d  12202  fsumabs  12232  fsumiun  12244  zproddc  12346  fprod2dlemstep  12389  fprod2d  12390  odd2np1  12640  ndvdssub  12697  bitsinv1lem  12728  dfgcd2  12791  nprm  12901  rpexp  12931  pc2dvds  13109  pcfac  13129  4sqlem12  13181  4sqlem17  13186  divsfval  13649  mulgaddcom  13949  mulginvcom  13950  ringinvnz1ne0  14354  lmss  15347  lmtopcnp  15351  txcn  15376  txlm  15380  xmettri2  15462  blin2  15533  metcnp3  15612  limcresi  15767  dvmptfsum  15826  logbgcd1irr  16069  lgsdir2lem2  16148  lgsne0  16157  2lgsoddprm  16232  2sqlem6  16239  2sqlem10  16244  uhgr0vb  16325  wlk1walkdom  16600  wlkv0  16610  wlklenvclwlk  16614  bj-stim  16774  bj-stan  16775  bj-stand  16776  bj-stal  16777  bj-sbimedh  16799  bj-vtoclgft  16803  elabgft1  16806  elabgf2  16808