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  2940  2ordpr  4646  regexmid  4657  ordsoexmid  4684  reg3exmid  4702  intasym  5147  relcoi1  5294  funres11  5428  cnvresid  5430  mpofvex  6401  df1st2  6415  df2nd2  6416  dftpos4  6494  tposf12  6500  frecabcl  6630  xp01disjl  6667  xpcomco  7077  1ndom2  7119  ominf  7153  sbthlem2  7228  djuunr  7357  eldju  7359  ctssdccl  7402  ctssdclemr  7403  omct  7408  ctssexmid  7441  rec1nq  7710  halfnqq  7725  caucvgsrlemasr  8105  axresscn  8175  0re  8274  gtso  8352  cnegexlem2  8449  uzn0  9870  indstr  9925  dfioo2  10307  fnn0nninf  10800  hashinfuni  11140  hashp1i  11175  cnrecnv  11595  rexanuz  11673  xrmaxiflemcom  11934  climdm  11980  sumsnf  12095  tanvalap  12394  egt2lt3  12466  lcmgcdlem  12774  3prm  12825  sqpweven  12872  2sqpwodd  12873  qnumval  12882  qdenval  12883  modxai  13114  xpnnen  13145  ennnfonelemhdmp1  13160  ennnfonelemss  13161  ennnfonelemnn0  13173  qnnen  13182  ctiunctal  13192  unct  13193  structcnvcnv  13228  setsslid  13263  prdsvallem  13485  prdsval  13486  xpsfrn  13563  xpsff1o2  13564  ringn0  14204  rmodislmodlem  14498  cnfldstr  14706  cnfldadd  14710  cnfldmul  14712  cnfldsub  14723  cnsubmlem  14726  cnsubglem  14727  zring0  14748  tgrest  15034  lmbr2  15079  cnptoprest  15104  lmff  15114  tx1cn  15134  tx2cn  15135  cnblcld  15400  cnfldms  15401  cnfldtopn  15404  tgioo  15419  reeff1o  15638  pilem1  15644  efhalfpi  15664  coseq0negpitopi  15701  konigsberglem2  16484  konigsberglem5  16487  pw1ninf  16765  012of  16767  pw1nct  16777  nnnninfen  16799  iswomninnlem  16834