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  2883  2ordpr  4556  regexmid  4567  ordsoexmid  4594  reg3exmid  4612  intasym  5050  relcoi1  5197  funres11  5326  cnvresid  5328  mpofvex  6256  df1st2  6272  df2nd2  6273  dftpos4  6316  tposf12  6322  frecabcl  6452  xp01disjl  6487  xpcomco  6880  ominf  6952  sbthlem2  7017  djuunr  7125  eldju  7127  ctssdccl  7170  ctssdclemr  7171  omct  7176  ctssexmid  7209  rec1nq  7455  halfnqq  7470  caucvgsrlemasr  7850  axresscn  7920  0re  8019  gtso  8098  cnegexlem2  8195  uzn0  9608  indstr  9658  dfioo2  10040  fnn0nninf  10509  hashinfuni  10848  hashp1i  10881  cnrecnv  11054  rexanuz  11132  xrmaxiflemcom  11392  climdm  11438  sumsnf  11552  tanvalap  11851  egt2lt3  11923  lcmgcdlem  12215  3prm  12266  sqpweven  12313  2sqpwodd  12314  qnumval  12323  qdenval  12324  xpnnen  12551  ennnfonelemhdmp1  12566  ennnfonelemss  12567  ennnfonelemnn0  12579  qnnen  12588  ctiunctal  12598  unct  12599  structcnvcnv  12634  setsslid  12669  xpsfrn  12933  xpsff1o2  12934  ringn0  13556  rmodislmodlem  13846  mpocnfldadd  14053  mpocnfldmul  14055  cnfldsub  14063  cnsubmlem  14066  cnsubglem  14067  zring0  14088  tgrest  14337  lmbr2  14382  cnptoprest  14407  lmff  14417  tx1cn  14437  tx2cn  14438  cnblcld  14703  tgioo  14714  reeff1o  14908  pilem1  14914  efhalfpi  14934  coseq0negpitopi  14971  012of  15486  pw1nct  15493  nnnninfen  15511  iswomninnlem  15539