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  2943  2ordpr  4651  regexmid  4662  ordsoexmid  4689  reg3exmid  4707  intasym  5152  relcoi1  5299  funres11  5433  cnvresid  5435  mpofvex  6414  df1st2  6428  df2nd2  6429  dftpos4  6507  tposf12  6513  frecabcl  6643  xp01disjl  6680  xpcomco  7090  1ndom2  7132  ominf  7166  sbthlem2  7241  djuunr  7370  eldju  7372  ctssdccl  7415  ctssdclemr  7416  omct  7421  ctssexmid  7454  rec1nq  7726  halfnqq  7741  caucvgsrlemasr  8121  axresscn  8191  0re  8290  gtso  8368  cnegexlem2  8466  uzn0  9891  indstr  9946  dfioo2  10329  fnn0nninf  10827  hashinfuni  11168  hashp1i  11203  cnrecnv  11623  rexanuz  11701  xrmaxiflemcom  11962  climdm  12008  sumsnf  12123  tanvalap  12422  egt2lt3  12494  lcmgcdlem  12802  3prm  12853  sqpweven  12900  2sqpwodd  12901  qnumval  12910  qdenval  12911  modxai  13142  xpnnen  13232  ennnfonelemhdmp1  13247  ennnfonelemss  13248  ennnfonelemnn0  13260  qnnen  13269  ctiunctal  13279  unct  13280  structcnvcnv  13315  setsslid  13350  prdsvallem  13567  xpsfrn  13617  xpsff1o2  13618  prdsval  14118  ringn0  14306  rmodislmodlem  14627  cnfldstr  14835  cnfldadd  14839  cnfldmul  14841  cnfldsub  14852  cnsubmlem  14855  cnsubglem  14856  zring0  14877  tgrest  15163  lmbr2  15208  cnptoprest  15233  lmff  15243  tx1cn  15263  tx2cn  15264  cnblcld  15529  cnfldms  15530  cnfldtopn  15533  tgioo  15548  reeff1o  15767  pilem1  15773  efhalfpi  15793  coseq0negpitopi  15830  konigsberglem2  16613  konigsberglem5  16616  pw1ninf  16904  012of  16906  pw1nct  16916  nnnninfen  16938  iswomninnlem  16973