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  2875  2ordpr  4541  regexmid  4552  ordsoexmid  4579  reg3exmid  4597  intasym  5031  relcoi1  5178  funres11  5307  cnvresid  5309  mpofvex  6228  df1st2  6244  df2nd2  6245  dftpos4  6288  tposf12  6294  frecabcl  6424  xp01disjl  6459  xpcomco  6852  ominf  6924  sbthlem2  6987  djuunr  7095  eldju  7097  ctssdccl  7140  ctssdclemr  7141  omct  7146  ctssexmid  7178  rec1nq  7424  halfnqq  7439  caucvgsrlemasr  7819  axresscn  7889  0re  7987  gtso  8066  cnegexlem2  8163  uzn0  9573  indstr  9623  dfioo2  10004  fnn0nninf  10468  hashinfuni  10789  hashp1i  10822  cnrecnv  10951  rexanuz  11029  xrmaxiflemcom  11289  climdm  11335  sumsnf  11449  tanvalap  11748  egt2lt3  11819  lcmgcdlem  12109  3prm  12160  sqpweven  12207  2sqpwodd  12208  qnumval  12217  qdenval  12218  xpnnen  12445  ennnfonelemhdmp1  12460  ennnfonelemss  12461  ennnfonelemnn0  12473  qnnen  12482  ctiunctal  12492  unct  12493  structcnvcnv  12528  setsslid  12563  xpsfrn  12826  xpsff1o2  12827  ringn0  13412  rmodislmodlem  13666  cnfldsub  13878  cnsubmlem  13881  cnsubglem  13882  zring0  13899  tgrest  14126  lmbr2  14171  cnptoprest  14196  lmff  14206  tx1cn  14226  tx2cn  14227  cnblcld  14492  tgioo  14503  reeff1o  14651  pilem1  14657  efhalfpi  14677  coseq0negpitopi  14714  012of  15204  pw1nct  15211  iswomninnlem  15256