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  2844  2ordpr  4495  regexmid  4506  ordsoexmid  4533  reg3exmid  4551  intasym  4982  relcoi1  5129  funres11  5254  cnvresid  5256  mpofvex  6163  df1st2  6178  df2nd2  6179  dftpos4  6222  tposf12  6228  frecabcl  6358  xp01disjl  6393  xpcomco  6783  ominf  6853  sbthlem2  6914  djuunr  7022  eldju  7024  ctssdccl  7067  ctssdclemr  7068  omct  7073  ctssexmid  7105  rec1nq  7327  halfnqq  7342  caucvgsrlemasr  7722  axresscn  7792  0re  7890  gtso  7968  cnegexlem2  8065  uzn0  9472  indstr  9522  dfioo2  9901  fnn0nninf  10362  hashinfuni  10679  hashp1i  10712  cnrecnv  10838  rexanuz  10916  xrmaxiflemcom  11176  climdm  11222  sumsnf  11336  tanvalap  11635  egt2lt3  11706  lcmgcdlem  11988  3prm  12039  sqpweven  12084  2sqpwodd  12085  qnumval  12094  qdenval  12095  xpnnen  12264  ennnfonelemhdmp1  12279  ennnfonelemss  12280  ennnfonelemnn0  12292  qnnen  12301  ctiunctal  12311  unct  12312  structcnvcnv  12347  setsslid  12381  tgrest  12710  lmbr2  12755  cnptoprest  12780  lmff  12790  tx1cn  12810  tx2cn  12811  cnblcld  13076  tgioo  13087  reeff1o  13235  pilem1  13241  efhalfpi  13261  coseq0negpitopi  13298  012of  13709  pw1nct  13717  iswomninnlem  13762