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  4616  regexmid  4627  ordsoexmid  4654  reg3exmid  4672  intasym  5113  relcoi1  5260  funres11  5393  cnvresid  5395  mpofvex  6357  df1st2  6371  df2nd2  6372  dftpos4  6415  tposf12  6421  frecabcl  6551  xp01disjl  6588  xpcomco  6993  1ndom2  7034  ominf  7066  sbthlem2  7133  djuunr  7241  eldju  7243  ctssdccl  7286  ctssdclemr  7287  omct  7292  ctssexmid  7325  rec1nq  7590  halfnqq  7605  caucvgsrlemasr  7985  axresscn  8055  0re  8154  gtso  8233  cnegexlem2  8330  uzn0  9746  indstr  9796  dfioo2  10178  fnn0nninf  10668  hashinfuni  11007  hashp1i  11040  cnrecnv  11429  rexanuz  11507  xrmaxiflemcom  11768  climdm  11814  sumsnf  11928  tanvalap  12227  egt2lt3  12299  lcmgcdlem  12607  3prm  12658  sqpweven  12705  2sqpwodd  12706  qnumval  12715  qdenval  12716  modxai  12947  xpnnen  12973  ennnfonelemhdmp1  12988  ennnfonelemss  12989  ennnfonelemnn0  13001  qnnen  13010  ctiunctal  13020  unct  13021  structcnvcnv  13056  setsslid  13091  prdsvallem  13313  prdsval  13314  xpsfrn  13391  xpsff1o2  13392  ringn0  14031  rmodislmodlem  14322  cnfldstr  14530  cnfldadd  14534  cnfldmul  14536  cnfldsub  14547  cnsubmlem  14550  cnsubglem  14551  zring0  14572  tgrest  14851  lmbr2  14896  cnptoprest  14921  lmff  14931  tx1cn  14951  tx2cn  14952  cnblcld  15217  cnfldms  15218  cnfldtopn  15221  tgioo  15236  reeff1o  15455  pilem1  15461  efhalfpi  15481  coseq0negpitopi  15518  pw1ninf  16384  012of  16386  pw1nct  16398  nnnninfen  16417  iswomninnlem  16447