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  2849  2ordpr  4501  regexmid  4512  ordsoexmid  4539  reg3exmid  4557  intasym  4988  relcoi1  5135  funres11  5260  cnvresid  5262  mpofvex  6171  df1st2  6187  df2nd2  6188  dftpos4  6231  tposf12  6237  frecabcl  6367  xp01disjl  6402  xpcomco  6792  ominf  6862  sbthlem2  6923  djuunr  7031  eldju  7033  ctssdccl  7076  ctssdclemr  7077  omct  7082  ctssexmid  7114  rec1nq  7336  halfnqq  7351  caucvgsrlemasr  7731  axresscn  7801  0re  7899  gtso  7977  cnegexlem2  8074  uzn0  9481  indstr  9531  dfioo2  9910  fnn0nninf  10372  hashinfuni  10690  hashp1i  10723  cnrecnv  10852  rexanuz  10930  xrmaxiflemcom  11190  climdm  11236  sumsnf  11350  tanvalap  11649  egt2lt3  11720  lcmgcdlem  12009  3prm  12060  sqpweven  12107  2sqpwodd  12108  qnumval  12117  qdenval  12118  xpnnen  12327  ennnfonelemhdmp1  12342  ennnfonelemss  12343  ennnfonelemnn0  12355  qnnen  12364  ctiunctal  12374  unct  12375  structcnvcnv  12410  setsslid  12444  tgrest  12809  lmbr2  12854  cnptoprest  12879  lmff  12889  tx1cn  12909  tx2cn  12910  cnblcld  13175  tgioo  13186  reeff1o  13334  pilem1  13340  efhalfpi  13360  coseq0negpitopi  13397  012of  13875  pw1nct  13883  iswomninnlem  13928