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  6538  tposf12  6544  frecabcl  6674  xp01disjl  6711  xpcomco  7128  1ndom2  7170  ominf  7204  sbthlem2  7280  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  9954  indstr  10009  dfioo2  10393  fnn0nninf  10896  hashinfuni  11238  hashp1i  11273  cnrecnv  11698  rexanuz  11776  xrmaxiflemcom  12040  climdm  12086  sumsnf  12201  tanvalap  12500  egt2lt3  12572  lcmgcdlem  12880  3prm  12931  oddpwdc  12979  sqpweven  12980  2sqpwodd  12981  qnumval  12990  qdenval  12991  modxai  13224  xpnnen  13343  ennnfonelemhdmp1  13358  ennnfonelemss  13359  ennnfonelemnn0  13371  qnnen  13380  ctiunctal  13390  unct  13391  structcnvcnv  13426  setsslid  13461  prdsvallem  13680  xpsfrn  13730  xpsff1o2  13731  gsum2dfilem2  14272  prdsval  14280  ringn0  14472  rmodislmodlem  14796  cnfldstr  15004  cnfldadd  15008  cnfldmul  15010  cnfldsub  15021  cnsubmlem  15024  cnsubglem  15025  zring0  15044  tgrest  15395  lmbr2  15440  cnptoprest  15465  lmff  15475  tx1cn  15495  tx2cn  15496  cnblcld  15761  cnfldms  15762  cnfldtopn  15765  tgioo  15780  reeff1o  15999  pilem1  16006  efhalfpi  16026  coseq0negpitopi  16063  ppiqltx  16281  bposlem6  16316  bposlem8  16318  konigsberglem2  16935  konigsberglem5  16938  pw1ninf  17226  012of  17228  pw1nct  17238  rabid1o  17239  stnot  17244  nnnninfen  17270  iswomninnlem  17306