Theorem mp2b 8

Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)

Hypotheses

Ref	Expression
mp2b.1	⊢ 𝜑
mp2b.2	⊢ (𝜑 → 𝜓)
mp2b.3	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
mp2b	⊢ 𝜒

Proof of Theorem mp2b

Step	Hyp	Ref	Expression
1		mp2b.1	. . 3 ⊢ 𝜑
2		mp2b.2	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	. 2 ⊢ 𝜓
4		mp2b.3	. 2 ⊢ (𝜓 → 𝜒)
5	3, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  eqvinc  2884  2ordpr  4557  regexmid  4568  ordsoexmid  4595  reg3exmid  4613  intasym  5051  relcoi1  5198  funres11  5327  cnvresid  5329  mpofvex  6260  df1st2  6274  df2nd2  6275  dftpos4  6318  tposf12  6324  frecabcl  6454  xp01disjl  6489  xpcomco  6882  ominf  6954  sbthlem2  7019  djuunr  7127  eldju  7129  ctssdccl  7172  ctssdclemr  7173  omct  7178  ctssexmid  7211  rec1nq  7457  halfnqq  7472  caucvgsrlemasr  7852  axresscn  7922  0re  8021  gtso  8100  cnegexlem2  8197  uzn0  9611  indstr  9661  dfioo2  10043  fnn0nninf  10512  hashinfuni  10851  hashp1i  10884  cnrecnv  11057  rexanuz  11135  xrmaxiflemcom  11395  climdm  11441  sumsnf  11555  tanvalap  11854  egt2lt3  11926  lcmgcdlem  12218  3prm  12269  sqpweven  12316  2sqpwodd  12317  qnumval  12326  qdenval  12327  xpnnen  12554  ennnfonelemhdmp1  12569  ennnfonelemss  12570  ennnfonelemnn0  12582  qnnen  12591  ctiunctal  12601  unct  12602  structcnvcnv  12637  setsslid  12672  xpsfrn  12936  xpsff1o2  12937  ringn0  13559  rmodislmodlem  13849  cnfldstr  14057  cnfldadd  14061  cnfldmul  14063  cnfldsub  14074  cnsubmlem  14077  cnsubglem  14078  zring0  14099  tgrest  14348  lmbr2  14393  cnptoprest  14418  lmff  14428  tx1cn  14448  tx2cn  14449  cnblcld  14714  cnfldms  14715  cnfldtopn  14718  tgioo  14733  reeff1o  14949  pilem1  14955  efhalfpi  14975  coseq0negpitopi  15012  012of  15556  pw1nct  15563  nnnninfen  15581  iswomninnlem  15609