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  2926  2ordpr  4617  regexmid  4628  ordsoexmid  4655  reg3exmid  4673  intasym  5116  relcoi1  5263  funres11  5396  cnvresid  5398  mpofvex  6362  df1st2  6376  df2nd2  6377  dftpos4  6420  tposf12  6426  frecabcl  6556  xp01disjl  6593  xpcomco  6998  1ndom2  7039  ominf  7071  sbthlem2  7141  djuunr  7249  eldju  7251  ctssdccl  7294  ctssdclemr  7295  omct  7300  ctssexmid  7333  rec1nq  7598  halfnqq  7613  caucvgsrlemasr  7993  axresscn  8063  0re  8162  gtso  8241  cnegexlem2  8338  uzn0  9755  indstr  9805  dfioo2  10187  fnn0nninf  10677  hashinfuni  11016  hashp1i  11050  cnrecnv  11442  rexanuz  11520  xrmaxiflemcom  11781  climdm  11827  sumsnf  11941  tanvalap  12240  egt2lt3  12312  lcmgcdlem  12620  3prm  12671  sqpweven  12718  2sqpwodd  12719  qnumval  12728  qdenval  12729  modxai  12960  xpnnen  12986  ennnfonelemhdmp1  13001  ennnfonelemss  13002  ennnfonelemnn0  13014  qnnen  13023  ctiunctal  13033  unct  13034  structcnvcnv  13069  setsslid  13104  prdsvallem  13326  prdsval  13327  xpsfrn  13404  xpsff1o2  13405  ringn0  14044  rmodislmodlem  14335  cnfldstr  14543  cnfldadd  14547  cnfldmul  14549  cnfldsub  14560  cnsubmlem  14563  cnsubglem  14564  zring0  14585  tgrest  14864  lmbr2  14909  cnptoprest  14934  lmff  14944  tx1cn  14964  tx2cn  14965  cnblcld  15230  cnfldms  15231  cnfldtopn  15234  tgioo  15249  reeff1o  15468  pilem1  15474  efhalfpi  15494  coseq0negpitopi  15531  pw1ninf  16468  012of  16470  pw1nct  16482  nnnninfen  16501  iswomninnlem  16531