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  2738  2ordpr  4330  regexmid  4341  ordsoexmid  4368  reg3exmid  4385  intasym  4803  relcoi1  4949  funres11  5072  cnvresid  5074  mpt2fvex  5955  df1st2  5966  df2nd2  5967  dftpos4  6010  tposf12  6016  frecabcl  6146  xpcomco  6522  ominf  6592  sbthlem2  6646  djuin  6735  djuunr  6737  eldju  6738  rec1nq  6933  halfnqq  6948  caucvgsrlemasr  7314  axresscn  7376  0re  7467  gtso  7543  cnegexlem2  7637  uzn0  9003  indstr  9050  dfioo2  9361  fnn0nninf  9808  hashinfuni  10149  hashp1i  10182  cnrecnv  10308  rexanuz  10385  climdm  10646  sumsnf  10764  lcmgcdlem  11139  3prm  11190  sqpweven  11233  2sqpwodd  11234  qnumval  11243  qdenval  11244  xpnnen  11287