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  2949  2ordpr  4666  regexmid  4677  ordsoexmid  4704  reg3exmid  4722  intasym  5167  relcoi1  5314  funres11  5448  cnvresid  5450  mpofvex  6431  df1st2  6445  df2nd2  6446  dftpos4  6524  tposf12  6530  frecabcl  6660  xp01disjl  6697  xpcomco  7114  1ndom2  7156  ominf  7190  sbthlem2  7265  djuunr  7396  eldju  7398  ctssdccl  7441  ctssdclemr  7442  omct  7447  ctssexmid  7480  rec1nq  7752  halfnqq  7767  caucvgsrlemasr  8147  axresscn  8217  0re  8316  gtso  8394  cnegexlem2  8492  uzn0  9917  indstr  9972  dfioo2  10355  fnn0nninf  10853  hashinfuni  11194  hashp1i  11229  cnrecnv  11654  rexanuz  11732  xrmaxiflemcom  11993  climdm  12039  sumsnf  12154  tanvalap  12453  egt2lt3  12525  lcmgcdlem  12833  3prm  12884  sqpweven  12931  2sqpwodd  12932  qnumval  12941  qdenval  12942  modxai  13173  xpnnen  13263  ennnfonelemhdmp1  13278  ennnfonelemss  13279  ennnfonelemnn0  13291  qnnen  13300  ctiunctal  13310  unct  13311  structcnvcnv  13346  setsslid  13381  prdsvallem  13598  xpsfrn  13648  xpsff1o2  13649  prdsval  14150  ringn0  14338  rmodislmodlem  14659  cnfldstr  14867  cnfldadd  14871  cnfldmul  14873  cnfldsub  14884  cnsubmlem  14887  cnsubglem  14888  zring0  14907  tgrest  15193  lmbr2  15238  cnptoprest  15263  lmff  15273  tx1cn  15293  tx2cn  15294  cnblcld  15559  cnfldms  15560  cnfldtopn  15563  tgioo  15578  reeff1o  15797  pilem1  15803  efhalfpi  15823  coseq0negpitopi  15860  konigsberglem2  16644  konigsberglem5  16647  pw1ninf  16935  012of  16937  pw1nct  16947  nnnninfen  16969  iswomninnlem  17004