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  2906  2ordpr  4593  regexmid  4604  ordsoexmid  4631  reg3exmid  4649  intasym  5089  relcoi1  5236  funres11  5369  cnvresid  5371  mpofvex  6321  df1st2  6335  df2nd2  6336  dftpos4  6379  tposf12  6385  frecabcl  6515  xp01disjl  6550  xpcomco  6953  1ndom2  6994  ominf  7026  sbthlem2  7093  djuunr  7201  eldju  7203  ctssdccl  7246  ctssdclemr  7247  omct  7252  ctssexmid  7285  rec1nq  7550  halfnqq  7565  caucvgsrlemasr  7945  axresscn  8015  0re  8114  gtso  8193  cnegexlem2  8290  uzn0  9706  indstr  9756  dfioo2  10138  fnn0nninf  10627  hashinfuni  10966  hashp1i  10999  cnrecnv  11387  rexanuz  11465  xrmaxiflemcom  11726  climdm  11772  sumsnf  11886  tanvalap  12185  egt2lt3  12257  lcmgcdlem  12565  3prm  12616  sqpweven  12663  2sqpwodd  12664  qnumval  12673  qdenval  12674  modxai  12905  xpnnen  12931  ennnfonelemhdmp1  12946  ennnfonelemss  12947  ennnfonelemnn0  12959  qnnen  12968  ctiunctal  12978  unct  12979  structcnvcnv  13014  setsslid  13049  prdsvallem  13271  prdsval  13272  xpsfrn  13349  xpsff1o2  13350  ringn0  13989  rmodislmodlem  14279  cnfldstr  14487  cnfldadd  14491  cnfldmul  14493  cnfldsub  14504  cnsubmlem  14507  cnsubglem  14508  zring0  14529  tgrest  14808  lmbr2  14853  cnptoprest  14878  lmff  14888  tx1cn  14908  tx2cn  14909  cnblcld  15174  cnfldms  15175  cnfldtopn  15178  tgioo  15193  reeff1o  15412  pilem1  15418  efhalfpi  15438  coseq0negpitopi  15475  012of  16268  pw1nct  16280  nnnninfen  16298  iswomninnlem  16328