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  4560  regexmid  4571  ordsoexmid  4598  reg3exmid  4616  intasym  5054  relcoi1  5201  funres11  5330  cnvresid  5332  mpofvex  6263  df1st2  6277  df2nd2  6278  dftpos4  6321  tposf12  6327  frecabcl  6457  xp01disjl  6492  xpcomco  6885  ominf  6957  sbthlem2  7024  djuunr  7132  eldju  7134  ctssdccl  7177  ctssdclemr  7178  omct  7183  ctssexmid  7216  rec1nq  7462  halfnqq  7477  caucvgsrlemasr  7857  axresscn  7927  0re  8026  gtso  8105  cnegexlem2  8202  uzn0  9617  indstr  9667  dfioo2  10049  fnn0nninf  10530  hashinfuni  10869  hashp1i  10902  cnrecnv  11075  rexanuz  11153  xrmaxiflemcom  11414  climdm  11460  sumsnf  11574  tanvalap  11873  egt2lt3  11945  lcmgcdlem  12245  3prm  12296  sqpweven  12343  2sqpwodd  12344  qnumval  12353  qdenval  12354  modxai  12585  xpnnen  12611  ennnfonelemhdmp1  12626  ennnfonelemss  12627  ennnfonelemnn0  12639  qnnen  12648  ctiunctal  12658  unct  12659  structcnvcnv  12694  setsslid  12729  xpsfrn  12993  xpsff1o2  12994  ringn0  13616  rmodislmodlem  13906  cnfldstr  14114  cnfldadd  14118  cnfldmul  14120  cnfldsub  14131  cnsubmlem  14134  cnsubglem  14135  zring0  14156  tgrest  14405  lmbr2  14450  cnptoprest  14475  lmff  14485  tx1cn  14505  tx2cn  14506  cnblcld  14771  cnfldms  14772  cnfldtopn  14775  tgioo  14790  reeff1o  15009  pilem1  15015  efhalfpi  15035  coseq0negpitopi  15072  012of  15640  pw1nct  15647  nnnninfen  15665  iswomninnlem  15693