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  2939  2ordpr  4645  regexmid  4656  ordsoexmid  4683  reg3exmid  4701  intasym  5146  relcoi1  5293  funres11  5427  cnvresid  5429  mpofvex  6400  df1st2  6414  df2nd2  6415  dftpos4  6493  tposf12  6499  frecabcl  6629  xp01disjl  6666  xpcomco  7076  1ndom2  7118  ominf  7152  sbthlem2  7227  djuunr  7356  eldju  7358  ctssdccl  7401  ctssdclemr  7402  omct  7407  ctssexmid  7440  rec1nq  7706  halfnqq  7721  caucvgsrlemasr  8101  axresscn  8171  0re  8270  gtso  8348  cnegexlem2  8445  uzn0  9866  indstr  9921  dfioo2  10303  fnn0nninf  10796  hashinfuni  11135  hashp1i  11170  cnrecnv  11588  rexanuz  11666  xrmaxiflemcom  11927  climdm  11973  sumsnf  12088  tanvalap  12387  egt2lt3  12459  lcmgcdlem  12767  3prm  12818  sqpweven  12865  2sqpwodd  12866  qnumval  12875  qdenval  12876  modxai  13107  xpnnen  13134  ennnfonelemhdmp1  13149  ennnfonelemss  13150  ennnfonelemnn0  13162  qnnen  13171  ctiunctal  13181  unct  13182  structcnvcnv  13217  setsslid  13252  prdsvallem  13474  prdsval  13475  xpsfrn  13552  xpsff1o2  13553  ringn0  14193  rmodislmodlem  14485  cnfldstr  14693  cnfldadd  14697  cnfldmul  14699  cnfldsub  14710  cnsubmlem  14713  cnsubglem  14714  zring0  14735  tgrest  15021  lmbr2  15066  cnptoprest  15091  lmff  15101  tx1cn  15121  tx2cn  15122  cnblcld  15387  cnfldms  15388  cnfldtopn  15391  tgioo  15406  reeff1o  15625  pilem1  15631  efhalfpi  15651  coseq0negpitopi  15688  konigsberglem2  16471  konigsberglem5  16474  pw1ninf  16752  012of  16754  pw1nct  16764  nnnninfen  16786  iswomninnlem  16821