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  2926  2ordpr  4616  regexmid  4627  ordsoexmid  4654  reg3exmid  4672  intasym  5113  relcoi1  5260  funres11  5393  cnvresid  5395  mpofvex  6357  df1st2  6371  df2nd2  6372  dftpos4  6415  tposf12  6421  frecabcl  6551  xp01disjl  6588  xpcomco  6993  1ndom2  7034  ominf  7066  sbthlem2  7136  djuunr  7244  eldju  7246  ctssdccl  7289  ctssdclemr  7290  omct  7295  ctssexmid  7328  rec1nq  7593  halfnqq  7608  caucvgsrlemasr  7988  axresscn  8058  0re  8157  gtso  8236  cnegexlem2  8333  uzn0  9750  indstr  9800  dfioo2  10182  fnn0nninf  10672  hashinfuni  11011  hashp1i  11045  cnrecnv  11436  rexanuz  11514  xrmaxiflemcom  11775  climdm  11821  sumsnf  11935  tanvalap  12234  egt2lt3  12306  lcmgcdlem  12614  3prm  12665  sqpweven  12712  2sqpwodd  12713  qnumval  12722  qdenval  12723  modxai  12954  xpnnen  12980  ennnfonelemhdmp1  12995  ennnfonelemss  12996  ennnfonelemnn0  13008  qnnen  13017  ctiunctal  13027  unct  13028  structcnvcnv  13063  setsslid  13098  prdsvallem  13320  prdsval  13321  xpsfrn  13398  xpsff1o2  13399  ringn0  14038  rmodislmodlem  14329  cnfldstr  14537  cnfldadd  14541  cnfldmul  14543  cnfldsub  14554  cnsubmlem  14557  cnsubglem  14558  zring0  14579  tgrest  14858  lmbr2  14903  cnptoprest  14928  lmff  14938  tx1cn  14958  tx2cn  14959  cnblcld  15224  cnfldms  15225  cnfldtopn  15228  tgioo  15243  reeff1o  15462  pilem1  15468  efhalfpi  15488  coseq0negpitopi  15525  pw1ninf  16414  012of  16416  pw1nct  16428  nnnninfen  16447  iswomninnlem  16477