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  2887  2ordpr  4561  regexmid  4572  ordsoexmid  4599  reg3exmid  4617  intasym  5055  relcoi1  5202  funres11  5331  cnvresid  5333  mpofvex  6264  df1st2  6278  df2nd2  6279  dftpos4  6322  tposf12  6328  frecabcl  6458  xp01disjl  6493  xpcomco  6886  ominf  6958  sbthlem2  7025  djuunr  7133  eldju  7135  ctssdccl  7178  ctssdclemr  7179  omct  7184  ctssexmid  7217  rec1nq  7464  halfnqq  7479  caucvgsrlemasr  7859  axresscn  7929  0re  8028  gtso  8107  cnegexlem2  8204  uzn0  9619  indstr  9669  dfioo2  10051  fnn0nninf  10532  hashinfuni  10871  hashp1i  10904  cnrecnv  11077  rexanuz  11155  xrmaxiflemcom  11416  climdm  11462  sumsnf  11576  tanvalap  11875  egt2lt3  11947  lcmgcdlem  12255  3prm  12306  sqpweven  12353  2sqpwodd  12354  qnumval  12363  qdenval  12364  modxai  12595  xpnnen  12621  ennnfonelemhdmp1  12636  ennnfonelemss  12637  ennnfonelemnn0  12649  qnnen  12658  ctiunctal  12668  unct  12669  structcnvcnv  12704  setsslid  12739  xpsfrn  13003  xpsff1o2  13004  ringn0  13626  rmodislmodlem  13916  cnfldstr  14124  cnfldadd  14128  cnfldmul  14130  cnfldsub  14141  cnsubmlem  14144  cnsubglem  14145  zring0  14166  tgrest  14415  lmbr2  14460  cnptoprest  14485  lmff  14495  tx1cn  14515  tx2cn  14516  cnblcld  14781  cnfldms  14782  cnfldtopn  14785  tgioo  14800  reeff1o  15019  pilem1  15025  efhalfpi  15045  coseq0negpitopi  15082  012of  15650  pw1nct  15657  nnnninfen  15675  iswomninnlem  15703