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  2718  2ordpr  4267  regexmid  4278  ordsoexmid  4305  reg3exmid  4322  intasym  4729  relcoi1  4869  funres11  4991  cnvresid  4993  mpt2fvex  5849  df1st2  5860  df2nd2  5861  dftpos4  5901  tposf12  5907  xpcomco  6323  rec1nq  6585  halfnqq  6600  caucvgsrlemasr  6966  axresscn  7028  0re  7119  gtso  7190  cnegexlem2  7284  uzn0  8634  indstr  8681  dfioo2  8997  cnrecnv  9797  rexanuz  9874  climdm  10134  lcmgcdlem  10459  3prm  10510  sqpweven  10553  2sqpwodd  10554