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  2943  2ordpr  4651  regexmid  4662  ordsoexmid  4689  reg3exmid  4707  intasym  5152  relcoi1  5299  funres11  5433  cnvresid  5435  mpofvex  6414  df1st2  6428  df2nd2  6429  dftpos4  6507  tposf12  6513  frecabcl  6643  xp01disjl  6680  xpcomco  7090  1ndom2  7132  ominf  7166  sbthlem2  7241  djuunr  7370  eldju  7372  ctssdccl  7415  ctssdclemr  7416  omct  7421  ctssexmid  7454  rec1nq  7726  halfnqq  7741  caucvgsrlemasr  8121  axresscn  8191  0re  8290  gtso  8368  cnegexlem2  8465  uzn0  9888  indstr  9943  dfioo2  10326  fnn0nninf  10824  hashinfuni  11165  hashp1i  11200  cnrecnv  11620  rexanuz  11698  xrmaxiflemcom  11959  climdm  12005  sumsnf  12120  tanvalap  12419  egt2lt3  12491  lcmgcdlem  12799  3prm  12850  sqpweven  12897  2sqpwodd  12898  qnumval  12907  qdenval  12908  modxai  13139  xpnnen  13229  ennnfonelemhdmp1  13244  ennnfonelemss  13245  ennnfonelemnn0  13257  qnnen  13266  ctiunctal  13276  unct  13277  structcnvcnv  13312  setsslid  13347  prdsvallem  13564  xpsfrn  13614  xpsff1o2  13615  prdsval  14115  ringn0  14303  rmodislmodlem  14624  cnfldstr  14832  cnfldadd  14836  cnfldmul  14838  cnfldsub  14849  cnsubmlem  14852  cnsubglem  14853  zring0  14874  tgrest  15160  lmbr2  15205  cnptoprest  15230  lmff  15240  tx1cn  15260  tx2cn  15261  cnblcld  15526  cnfldms  15527  cnfldtopn  15530  tgioo  15545  reeff1o  15764  pilem1  15770  efhalfpi  15790  coseq0negpitopi  15827  konigsberglem2  16610  konigsberglem5  16613  pw1ninf  16891  012of  16893  pw1nct  16903  nnnninfen  16925  iswomninnlem  16960