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  4673  regexmid  4684  ordsoexmid  4711  reg3exmid  4729  intasym  5175  relcoi1  5322  funres11  5456  cnvresid  5458  mpofvex  6445  df1st2  6459  df2nd2  6460  dftpos4  6539  tposf12  6545  frecabcl  6675  xp01disjl  6712  xpcomco  7130  1ndom2  7172  ominf  7206  sbthlem2  7282  djuunr  7412  eldju  7414  ctssdccl  7457  ctssdclemr  7458  omct  7463  ctssexmid  7496  rec1nq  7768  halfnqq  7783  caucvgsrlemasr  8163  axresscn  8233  0re  8332  gtso  8410  cnegexlem2  8509  uzn0  9953  indstr  10008  dfioo2  10392  fnn0nninf  10895  hashinfuni  11237  hashp1i  11272  cnrecnv  11697  rexanuz  11775  xrmaxiflemcom  12039  climdm  12085  sumsnf  12200  tanvalap  12499  egt2lt3  12571  lcmgcdlem  12879  3prm  12930  oddpwdc  12978  sqpweven  12979  2sqpwodd  12980  qnumval  12989  qdenval  12990  modxai  13223  xpnnen  13342  ennnfonelemhdmp1  13357  ennnfonelemss  13358  ennnfonelemnn0  13370  qnnen  13379  ctiunctal  13389  unct  13390  structcnvcnv  13425  setsslid  13460  prdsvallem  13679  xpsfrn  13729  xpsff1o2  13730  gsum2dfilem2  14271  prdsval  14279  ringn0  14471  rmodislmodlem  14795  cnfldstr  15003  cnfldadd  15007  cnfldmul  15009  cnfldsub  15020  cnsubmlem  15023  cnsubglem  15024  zring0  15043  tgrest  15412  lmbr2  15457  cnptoprest  15482  lmff  15492  tx1cn  15512  tx2cn  15513  cnblcld  15778  cnfldms  15779  cnfldtopn  15782  tgioo  15797  reeff1o  16016  pilem1  16023  efhalfpi  16043  coseq0negpitopi  16080  ppiqltx  16298  bposlem6  16333  bposlem8  16335  konigsberglem2  16952  konigsberglem5  16955  pw1ninf  17243  012of  17245  pw1nct  17255  rabid1o  17256  stnot  17261  nnnninfen  17287  iswomninnlem  17323