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  2927  2ordpr  4620  regexmid  4631  ordsoexmid  4658  reg3exmid  4676  intasym  5119  relcoi1  5266  funres11  5399  cnvresid  5401  mpofvex  6365  df1st2  6379  df2nd2  6380  dftpos4  6424  tposf12  6430  frecabcl  6560  xp01disjl  6597  xpcomco  7005  1ndom2  7046  ominf  7078  sbthlem2  7148  djuunr  7256  eldju  7258  ctssdccl  7301  ctssdclemr  7302  omct  7307  ctssexmid  7340  rec1nq  7605  halfnqq  7620  caucvgsrlemasr  8000  axresscn  8070  0re  8169  gtso  8248  cnegexlem2  8345  uzn0  9762  indstr  9817  dfioo2  10199  fnn0nninf  10690  hashinfuni  11029  hashp1i  11064  cnrecnv  11461  rexanuz  11539  xrmaxiflemcom  11800  climdm  11846  sumsnf  11960  tanvalap  12259  egt2lt3  12331  lcmgcdlem  12639  3prm  12690  sqpweven  12737  2sqpwodd  12738  qnumval  12747  qdenval  12748  modxai  12979  xpnnen  13005  ennnfonelemhdmp1  13020  ennnfonelemss  13021  ennnfonelemnn0  13033  qnnen  13042  ctiunctal  13052  unct  13053  structcnvcnv  13088  setsslid  13123  prdsvallem  13345  prdsval  13346  xpsfrn  13423  xpsff1o2  13424  ringn0  14063  rmodislmodlem  14354  cnfldstr  14562  cnfldadd  14566  cnfldmul  14568  cnfldsub  14579  cnsubmlem  14582  cnsubglem  14583  zring0  14604  tgrest  14883  lmbr2  14928  cnptoprest  14953  lmff  14963  tx1cn  14983  tx2cn  14984  cnblcld  15249  cnfldms  15250  cnfldtopn  15253  tgioo  15268  reeff1o  15487  pilem1  15493  efhalfpi  15513  coseq0negpitopi  15550  pw1ninf  16526  012of  16528  pw1nct  16540  nnnninfen  16559  iswomninnlem  16589