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  2887  2ordpr  4561  regexmid  4572  ordsoexmid  4599  reg3exmid  4617  intasym  5055  relcoi1  5202  funres11  5331  cnvresid  5333  mpofvex  6272  df1st2  6286  df2nd2  6287  dftpos4  6330  tposf12  6336  frecabcl  6466  xp01disjl  6501  xpcomco  6894  ominf  6966  sbthlem2  7033  djuunr  7141  eldju  7143  ctssdccl  7186  ctssdclemr  7187  omct  7192  ctssexmid  7225  rec1nq  7481  halfnqq  7496  caucvgsrlemasr  7876  axresscn  7946  0re  8045  gtso  8124  cnegexlem2  8221  uzn0  9636  indstr  9686  dfioo2  10068  fnn0nninf  10549  hashinfuni  10888  hashp1i  10921  cnrecnv  11094  rexanuz  11172  xrmaxiflemcom  11433  climdm  11479  sumsnf  11593  tanvalap  11892  egt2lt3  11964  lcmgcdlem  12272  3prm  12323  sqpweven  12370  2sqpwodd  12371  qnumval  12380  qdenval  12381  modxai  12612  xpnnen  12638  ennnfonelemhdmp1  12653  ennnfonelemss  12654  ennnfonelemnn0  12666  qnnen  12675  ctiunctal  12685  unct  12686  structcnvcnv  12721  setsslid  12756  prdsvallem  12976  prdsval  12977  xpsfrn  13054  xpsff1o2  13055  ringn0  13694  rmodislmodlem  13984  cnfldstr  14192  cnfldadd  14196  cnfldmul  14198  cnfldsub  14209  cnsubmlem  14212  cnsubglem  14213  zring0  14234  tgrest  14513  lmbr2  14558  cnptoprest  14583  lmff  14593  tx1cn  14613  tx2cn  14614  cnblcld  14879  cnfldms  14880  cnfldtopn  14883  tgioo  14898  reeff1o  15117  pilem1  15123  efhalfpi  15143  coseq0negpitopi  15180  012of  15748  pw1nct  15758  nnnninfen  15776  iswomninnlem  15806