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  4615  regexmid  4626  ordsoexmid  4653  reg3exmid  4671  intasym  5112  relcoi1  5259  funres11  5392  cnvresid  5394  mpofvex  6349  df1st2  6363  df2nd2  6364  dftpos4  6407  tposf12  6413  frecabcl  6543  xp01disjl  6578  xpcomco  6981  1ndom2  7022  ominf  7054  sbthlem2  7121  djuunr  7229  eldju  7231  ctssdccl  7274  ctssdclemr  7275  omct  7280  ctssexmid  7313  rec1nq  7578  halfnqq  7593  caucvgsrlemasr  7973  axresscn  8043  0re  8142  gtso  8221  cnegexlem2  8318  uzn0  9734  indstr  9784  dfioo2  10166  fnn0nninf  10655  hashinfuni  10994  hashp1i  11027  cnrecnv  11416  rexanuz  11494  xrmaxiflemcom  11755  climdm  11801  sumsnf  11915  tanvalap  12214  egt2lt3  12286  lcmgcdlem  12594  3prm  12645  sqpweven  12692  2sqpwodd  12693  qnumval  12702  qdenval  12703  modxai  12934  xpnnen  12960  ennnfonelemhdmp1  12975  ennnfonelemss  12976  ennnfonelemnn0  12988  qnnen  12997  ctiunctal  13007  unct  13008  structcnvcnv  13043  setsslid  13078  prdsvallem  13300  prdsval  13301  xpsfrn  13378  xpsff1o2  13379  ringn0  14018  rmodislmodlem  14308  cnfldstr  14516  cnfldadd  14520  cnfldmul  14522  cnfldsub  14533  cnsubmlem  14536  cnsubglem  14537  zring0  14558  tgrest  14837  lmbr2  14882  cnptoprest  14907  lmff  14917  tx1cn  14937  tx2cn  14938  cnblcld  15203  cnfldms  15204  cnfldtopn  15207  tgioo  15222  reeff1o  15441  pilem1  15447  efhalfpi  15467  coseq0negpitopi  15504  012of  16316  pw1nct  16328  nnnninfen  16346  iswomninnlem  16376