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  2853  2ordpr  4508  regexmid  4519  ordsoexmid  4546  reg3exmid  4564  intasym  4995  relcoi1  5142  funres11  5270  cnvresid  5272  mpofvex  6182  df1st2  6198  df2nd2  6199  dftpos4  6242  tposf12  6248  frecabcl  6378  xp01disjl  6413  xpcomco  6804  ominf  6874  sbthlem2  6935  djuunr  7043  eldju  7045  ctssdccl  7088  ctssdclemr  7089  omct  7094  ctssexmid  7126  rec1nq  7357  halfnqq  7372  caucvgsrlemasr  7752  axresscn  7822  0re  7920  gtso  7998  cnegexlem2  8095  uzn0  9502  indstr  9552  dfioo2  9931  fnn0nninf  10393  hashinfuni  10711  hashp1i  10745  cnrecnv  10874  rexanuz  10952  xrmaxiflemcom  11212  climdm  11258  sumsnf  11372  tanvalap  11671  egt2lt3  11742  lcmgcdlem  12031  3prm  12082  sqpweven  12129  2sqpwodd  12130  qnumval  12139  qdenval  12140  xpnnen  12349  ennnfonelemhdmp1  12364  ennnfonelemss  12365  ennnfonelemnn0  12377  qnnen  12386  ctiunctal  12396  unct  12397  structcnvcnv  12432  setsslid  12466  tgrest  12963  lmbr2  13008  cnptoprest  13033  lmff  13043  tx1cn  13063  tx2cn  13064  cnblcld  13329  tgioo  13340  reeff1o  13488  pilem1  13494  efhalfpi  13514  coseq0negpitopi  13551  012of  14028  pw1nct  14036  iswomninnlem  14081