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  11163  rexanuz  11241  xrmaxiflemcom  11502  climdm  11548  sumsnf  11662  tanvalap  11961  egt2lt3  12033  lcmgcdlem  12341  3prm  12392  sqpweven  12439  2sqpwodd  12440  qnumval  12449  qdenval  12450  modxai  12681  xpnnen  12707  ennnfonelemhdmp1  12722  ennnfonelemss  12723  ennnfonelemnn0  12735  qnnen  12744  ctiunctal  12754  unct  12755  structcnvcnv  12790  setsslid  12825  prdsvallem  13046  prdsval  13047  xpsfrn  13124  xpsff1o2  13125  ringn0  13764  rmodislmodlem  14054  cnfldstr  14262  cnfldadd  14266  cnfldmul  14268  cnfldsub  14279  cnsubmlem  14282  cnsubglem  14283  zring0  14304  tgrest  14583  lmbr2  14628  cnptoprest  14653  lmff  14663  tx1cn  14683  tx2cn  14684  cnblcld  14949  cnfldms  14950  cnfldtopn  14953  tgioo  14968  reeff1o  15187  pilem1  15193  efhalfpi  15213  coseq0negpitopi  15250  012of  15863  pw1nct  15873  nnnninfen  15891  iswomninnlem  15921