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  2929  2ordpr  4622  regexmid  4633  ordsoexmid  4660  reg3exmid  4678  intasym  5121  relcoi1  5268  funres11  5402  cnvresid  5404  mpofvex  6370  df1st2  6384  df2nd2  6385  dftpos4  6429  tposf12  6435  frecabcl  6565  xp01disjl  6602  xpcomco  7010  1ndom2  7051  ominf  7085  sbthlem2  7157  djuunr  7265  eldju  7267  ctssdccl  7310  ctssdclemr  7311  omct  7316  ctssexmid  7349  rec1nq  7615  halfnqq  7630  caucvgsrlemasr  8010  axresscn  8080  0re  8179  gtso  8258  cnegexlem2  8355  uzn0  9772  indstr  9827  dfioo2  10209  fnn0nninf  10701  hashinfuni  11040  hashp1i  11075  cnrecnv  11488  rexanuz  11566  xrmaxiflemcom  11827  climdm  11873  sumsnf  11988  tanvalap  12287  egt2lt3  12359  lcmgcdlem  12667  3prm  12718  sqpweven  12765  2sqpwodd  12766  qnumval  12775  qdenval  12776  modxai  13007  xpnnen  13033  ennnfonelemhdmp1  13048  ennnfonelemss  13049  ennnfonelemnn0  13061  qnnen  13070  ctiunctal  13080  unct  13081  structcnvcnv  13116  setsslid  13151  prdsvallem  13373  prdsval  13374  xpsfrn  13451  xpsff1o2  13452  ringn0  14092  rmodislmodlem  14383  cnfldstr  14591  cnfldadd  14595  cnfldmul  14597  cnfldsub  14608  cnsubmlem  14611  cnsubglem  14612  zring0  14633  tgrest  14912  lmbr2  14957  cnptoprest  14982  lmff  14992  tx1cn  15012  tx2cn  15013  cnblcld  15278  cnfldms  15279  cnfldtopn  15282  tgioo  15297  reeff1o  15516  pilem1  15522  efhalfpi  15542  coseq0negpitopi  15579  konigsberglem2  16359  konigsberglem5  16362  pw1ninf  16641  012of  16643  pw1nct  16655  nnnninfen  16674  iswomninnlem  16705