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  8502  uzn0  9938  indstr  9993  dfioo2  10376  fnn0nninf  10875  hashinfuni  11216  hashp1i  11251  cnrecnv  11676  rexanuz  11754  xrmaxiflemcom  12015  climdm  12061  sumsnf  12176  tanvalap  12475  egt2lt3  12547  lcmgcdlem  12855  3prm  12906  sqpweven  12953  2sqpwodd  12954  qnumval  12963  qdenval  12964  modxai  13195  xpnnen  13285  ennnfonelemhdmp1  13300  ennnfonelemss  13301  ennnfonelemnn0  13313  qnnen  13322  ctiunctal  13332  unct  13333  structcnvcnv  13368  setsslid  13403  prdsvallem  13621  xpsfrn  13671  xpsff1o2  13672  prdsval  14173  ringn0  14365  rmodislmodlem  14687  cnfldstr  14895  cnfldadd  14899  cnfldmul  14901  cnfldsub  14912  cnsubmlem  14915  cnsubglem  14916  zring0  14935  tgrest  15270  lmbr2  15315  cnptoprest  15340  lmff  15350  tx1cn  15370  tx2cn  15371  cnblcld  15636  cnfldms  15637  cnfldtopn  15640  tgioo  15655  reeff1o  15874  pilem1  15880  efhalfpi  15900  coseq0negpitopi  15937  konigsberglem2  16730  konigsberglem5  16733  pw1ninf  17021  012of  17023  pw1nct  17033  rabid1o  17034  stnot  17039  nnnninfen  17064  iswomninnlem  17099