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 7	. 2 |- ps
4		mp2b.3	. 2 |- ( ps -> ch )
5	3, 4	ax-mp 7	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 7

This theorem is referenced by:  eqvinc  2776  2ordpr  4397  regexmid  4408  ordsoexmid  4435  reg3exmid  4452  intasym  4879  relcoi1  5026  funres11  5151  cnvresid  5153  mpofvex  6053  df1st2  6068  df2nd2  6069  dftpos4  6112  tposf12  6118  frecabcl  6248  xp01disjl  6283  xpcomco  6671  ominf  6741  sbthlem2  6796  djuunr  6901  eldju  6903  ctssdccl  6946  ctssdclemr  6947  ctssexmid  6972  rec1nq  7145  halfnqq  7160  caucvgsrlemasr  7526  axresscn  7589  0re  7684  gtso  7760  cnegexlem2  7855  uzn0  9237  indstr  9284  dfioo2  9644  fnn0nninf  10097  hashinfuni  10410  hashp1i  10443  cnrecnv  10569  rexanuz  10646  xrmaxiflemcom  10904  climdm  10950  sumsnf  11064  tanvalap  11260  egt2lt3  11328  lcmgcdlem  11598  3prm  11649  sqpweven  11692  2sqpwodd  11693  qnumval  11702  qdenval  11703  xpnnen  11746  ennnfonelemhdmp1  11761  ennnfonelemss  11762  ennnfonelemnn0  11774  qnnen  11783  unct  11791  structcnvcnv  11812  setsslid  11846  tgrest  12175  lmbr2  12219  cnptoprest  12244  lmff  12254  tx1cn  12274  tx2cn  12275  cnblcld  12518  tgioo  12526  isomninnlem  12906