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

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  eqvinc  2949  2ordpr  4671  regexmid  4682  ordsoexmid  4709  reg3exmid  4727  intasym  5172  relcoi1  5319  funres11  5453  cnvresid  5455  mpofvex  6441  df1st2  6455  df2nd2  6456  dftpos4  6534  tposf12  6540  frecabcl  6670  xp01disjl  6707  xpcomco  7124  1ndom2  7166  ominf  7200  sbthlem2  7275  djuunr  7406  eldju  7408  ctssdccl  7451  ctssdclemr  7452  omct  7457  ctssexmid  7490  rec1nq  7762  halfnqq  7777  caucvgsrlemasr  8157  axresscn  8227  0re  8326  gtso  8404  cnegexlem2  8503  uzn0  9947  indstr  10002  dfioo2  10386  fnn0nninf  10888  hashinfuni  11230  hashp1i  11265  cnrecnv  11690  rexanuz  11768  xrmaxiflemcom  12031  climdm  12077  sumsnf  12192  tanvalap  12491  egt2lt3  12563  lcmgcdlem  12871  3prm  12922  oddpwdc  12970  sqpweven  12971  2sqpwodd  12972  qnumval  12981  qdenval  12982  modxai  13215  xpnnen  13334  ennnfonelemhdmp1  13349  ennnfonelemss  13350  ennnfonelemnn0  13362  qnnen  13371  ctiunctal  13381  unct  13382  structcnvcnv  13417  setsslid  13452  prdsvallem  13670  xpsfrn  13720  xpsff1o2  13721  prdsval  14222  ringn0  14414  rmodislmodlem  14736  cnfldstr  14944  cnfldadd  14948  cnfldmul  14950  cnfldsub  14961  cnsubmlem  14964  cnsubglem  14965  zring0  14984  tgrest  15319  lmbr2  15364  cnptoprest  15389  lmff  15399  tx1cn  15419  tx2cn  15420  cnblcld  15685  cnfldms  15686  cnfldtopn  15689  tgioo  15704  reeff1o  15923  pilem1  15930  efhalfpi  15950  coseq0negpitopi  15987  ppiqltx  16183  konigsberglem2  16828  konigsberglem5  16831  pw1ninf  17119  012of  17121  pw1nct  17131  rabid1o  17132  stnot  17137  nnnninfen  17162  iswomninnlem  17197