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  2900  2ordpr  4585  regexmid  4596  ordsoexmid  4623  reg3exmid  4641  intasym  5081  relcoi1  5228  funres11  5360  cnvresid  5362  mpofvex  6309  df1st2  6323  df2nd2  6324  dftpos4  6367  tposf12  6373  frecabcl  6503  xp01disjl  6538  xpcomco  6941  1ndom2  6982  ominf  7014  sbthlem2  7081  djuunr  7189  eldju  7191  ctssdccl  7234  ctssdclemr  7235  omct  7240  ctssexmid  7273  rec1nq  7538  halfnqq  7553  caucvgsrlemasr  7933  axresscn  8003  0re  8102  gtso  8181  cnegexlem2  8278  uzn0  9694  indstr  9744  dfioo2  10126  fnn0nninf  10615  hashinfuni  10954  hashp1i  10987  cnrecnv  11306  rexanuz  11384  xrmaxiflemcom  11645  climdm  11691  sumsnf  11805  tanvalap  12104  egt2lt3  12176  lcmgcdlem  12484  3prm  12535  sqpweven  12582  2sqpwodd  12583  qnumval  12592  qdenval  12593  modxai  12824  xpnnen  12850  ennnfonelemhdmp1  12865  ennnfonelemss  12866  ennnfonelemnn0  12878  qnnen  12887  ctiunctal  12897  unct  12898  structcnvcnv  12933  setsslid  12968  prdsvallem  13189  prdsval  13190  xpsfrn  13267  xpsff1o2  13268  ringn0  13907  rmodislmodlem  14197  cnfldstr  14405  cnfldadd  14409  cnfldmul  14411  cnfldsub  14422  cnsubmlem  14425  cnsubglem  14426  zring0  14447  tgrest  14726  lmbr2  14771  cnptoprest  14796  lmff  14806  tx1cn  14826  tx2cn  14827  cnblcld  15092  cnfldms  15093  cnfldtopn  15096  tgioo  15111  reeff1o  15330  pilem1  15336  efhalfpi  15356  coseq0negpitopi  15393  012of  16100  pw1nct  16112  nnnninfen  16130  iswomninnlem  16160