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  2858  2ordpr  4517  regexmid  4528  ordsoexmid  4555  reg3exmid  4573  intasym  5005  relcoi1  5152  funres11  5280  cnvresid  5282  mpofvex  6194  df1st2  6210  df2nd2  6211  dftpos4  6254  tposf12  6260  frecabcl  6390  xp01disjl  6425  xpcomco  6816  ominf  6886  sbthlem2  6947  djuunr  7055  eldju  7057  ctssdccl  7100  ctssdclemr  7101  omct  7106  ctssexmid  7138  rec1nq  7369  halfnqq  7384  caucvgsrlemasr  7764  axresscn  7834  0re  7932  gtso  8010  cnegexlem2  8107  uzn0  9514  indstr  9564  dfioo2  9943  fnn0nninf  10405  hashinfuni  10723  hashp1i  10756  cnrecnv  10885  rexanuz  10963  xrmaxiflemcom  11223  climdm  11269  sumsnf  11383  tanvalap  11682  egt2lt3  11753  lcmgcdlem  12042  3prm  12093  sqpweven  12140  2sqpwodd  12141  qnumval  12150  qdenval  12151  xpnnen  12360  ennnfonelemhdmp1  12375  ennnfonelemss  12376  ennnfonelemnn0  12388  qnnen  12397  ctiunctal  12407  unct  12408  structcnvcnv  12443  setsslid  12477  ringn0  13029  tgrest  13220  lmbr2  13265  cnptoprest  13290  lmff  13300  tx1cn  13320  tx2cn  13321  cnblcld  13586  tgioo  13597  reeff1o  13745  pilem1  13751  efhalfpi  13771  coseq0negpitopi  13808  012of  14285  pw1nct  14293  iswomninnlem  14338