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  2803  2ordpr  4434  regexmid  4445  ordsoexmid  4472  reg3exmid  4489  intasym  4918  relcoi1  5065  funres11  5190  cnvresid  5192  mpofvex  6094  df1st2  6109  df2nd2  6110  dftpos4  6153  tposf12  6159  frecabcl  6289  xp01disjl  6324  xpcomco  6713  ominf  6783  sbthlem2  6839  djuunr  6944  eldju  6946  ctssdccl  6989  ctssdclemr  6990  omct  6995  ctssexmid  7017  rec1nq  7196  halfnqq  7211  caucvgsrlemasr  7591  axresscn  7661  0re  7759  gtso  7836  cnegexlem2  7931  uzn0  9334  indstr  9381  dfioo2  9750  fnn0nninf  10203  hashinfuni  10516  hashp1i  10549  cnrecnv  10675  rexanuz  10753  xrmaxiflemcom  11011  climdm  11057  sumsnf  11171  tanvalap  11404  egt2lt3  11475  lcmgcdlem  11747  3prm  11798  sqpweven  11842  2sqpwodd  11843  qnumval  11852  qdenval  11853  xpnnen  11896  ennnfonelemhdmp1  11911  ennnfonelemss  11912  ennnfonelemnn0  11924  qnnen  11933  unct  11943  structcnvcnv  11964  setsslid  11998  tgrest  12327  lmbr2  12372  cnptoprest  12397  lmff  12407  tx1cn  12427  tx2cn  12428  cnblcld  12693  tgioo  12704  pilem1  12849  efhalfpi  12869  coseq0negpitopi  12906  isomninnlem  13214