Theorem mp2b 8

Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)

Hypotheses

Ref	Expression
mp2b.1	|- ph
mp2b.2	|- ( ph -> ps )
mp2b.3	|- ( ps -> ch )

Assertion

Ref	Expression
mp2b	|- ch

Proof of Theorem mp2b

Step	Hyp	Ref	Expression
1		mp2b.1	. . 3 |- ph
2		mp2b.2	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 5	. 2 |- ps
4		mp2b.3	. 2 |- ( ps -> ch )
5	3, 4	ax-mp 5	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  eqvinc  2895  2ordpr  4571  regexmid  4582  ordsoexmid  4609  reg3exmid  4627  intasym  5066  relcoi1  5213  funres11  5345  cnvresid  5347  mpofvex  6290  df1st2  6304  df2nd2  6305  dftpos4  6348  tposf12  6354  frecabcl  6484  xp01disjl  6519  xpcomco  6920  ominf  6992  sbthlem2  7059  djuunr  7167  eldju  7169  ctssdccl  7212  ctssdclemr  7213  omct  7218  ctssexmid  7251  rec1nq  7507  halfnqq  7522  caucvgsrlemasr  7902  axresscn  7972  0re  8071  gtso  8150  cnegexlem2  8247  uzn0  9663  indstr  9713  dfioo2  10095  fnn0nninf  10581  hashinfuni  10920  hashp1i  10953  cnrecnv  11192  rexanuz  11270  xrmaxiflemcom  11531  climdm  11577  sumsnf  11691  tanvalap  11990  egt2lt3  12062  lcmgcdlem  12370  3prm  12421  sqpweven  12468  2sqpwodd  12469  qnumval  12478  qdenval  12479  modxai  12710  xpnnen  12736  ennnfonelemhdmp1  12751  ennnfonelemss  12752  ennnfonelemnn0  12764  qnnen  12773  ctiunctal  12783  unct  12784  structcnvcnv  12819  setsslid  12854  prdsvallem  13075  prdsval  13076  xpsfrn  13153  xpsff1o2  13154  ringn0  13793  rmodislmodlem  14083  cnfldstr  14291  cnfldadd  14295  cnfldmul  14297  cnfldsub  14308  cnsubmlem  14311  cnsubglem  14312  zring0  14333  tgrest  14612  lmbr2  14657  cnptoprest  14682  lmff  14692  tx1cn  14712  tx2cn  14713  cnblcld  14978  cnfldms  14979  cnfldtopn  14982  tgioo  14997  reeff1o  15216  pilem1  15222  efhalfpi  15242  coseq0negpitopi  15279  012of  15892  pw1nct  15902  nnnninfen  15920  iswomninnlem  15950