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  2930  2ordpr  4628  regexmid  4639  ordsoexmid  4666  reg3exmid  4684  intasym  5128  relcoi1  5275  funres11  5409  cnvresid  5411  mpofvex  6379  df1st2  6393  df2nd2  6394  dftpos4  6472  tposf12  6478  frecabcl  6608  xp01disjl  6645  xpcomco  7053  1ndom2  7094  ominf  7128  sbthlem2  7200  djuunr  7308  eldju  7310  ctssdccl  7353  ctssdclemr  7354  omct  7359  ctssexmid  7392  rec1nq  7658  halfnqq  7673  caucvgsrlemasr  8053  axresscn  8123  0re  8222  gtso  8300  cnegexlem2  8397  uzn0  9816  indstr  9871  dfioo2  10253  fnn0nninf  10746  hashinfuni  11085  hashp1i  11120  cnrecnv  11533  rexanuz  11611  xrmaxiflemcom  11872  climdm  11918  sumsnf  12033  tanvalap  12332  egt2lt3  12404  lcmgcdlem  12712  3prm  12763  sqpweven  12810  2sqpwodd  12811  qnumval  12820  qdenval  12821  modxai  13052  xpnnen  13078  ennnfonelemhdmp1  13093  ennnfonelemss  13094  ennnfonelemnn0  13106  qnnen  13115  ctiunctal  13125  unct  13126  structcnvcnv  13161  setsslid  13196  prdsvallem  13418  prdsval  13419  xpsfrn  13496  xpsff1o2  13497  ringn0  14137  rmodislmodlem  14429  cnfldstr  14637  cnfldadd  14641  cnfldmul  14643  cnfldsub  14654  cnsubmlem  14657  cnsubglem  14658  zring0  14679  tgrest  14963  lmbr2  15008  cnptoprest  15033  lmff  15043  tx1cn  15063  tx2cn  15064  cnblcld  15329  cnfldms  15330  cnfldtopn  15333  tgioo  15348  reeff1o  15567  pilem1  15573  efhalfpi  15593  coseq0negpitopi  15630  konigsberglem2  16413  konigsberglem5  16416  pw1ninf  16694  012of  16696  pw1nct  16708  nnnninfen  16730  iswomninnlem  16765