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  2861  2ordpr  4524  regexmid  4535  ordsoexmid  4562  reg3exmid  4580  intasym  5014  relcoi1  5161  funres11  5289  cnvresid  5291  mpofvex  6204  df1st2  6220  df2nd2  6221  dftpos4  6264  tposf12  6270  frecabcl  6400  xp01disjl  6435  xpcomco  6826  ominf  6896  sbthlem2  6957  djuunr  7065  eldju  7067  ctssdccl  7110  ctssdclemr  7111  omct  7116  ctssexmid  7148  rec1nq  7394  halfnqq  7409  caucvgsrlemasr  7789  axresscn  7859  0re  7957  gtso  8036  cnegexlem2  8133  uzn0  9543  indstr  9593  dfioo2  9974  fnn0nninf  10437  hashinfuni  10757  hashp1i  10790  cnrecnv  10919  rexanuz  10997  xrmaxiflemcom  11257  climdm  11303  sumsnf  11417  tanvalap  11716  egt2lt3  11787  lcmgcdlem  12077  3prm  12128  sqpweven  12175  2sqpwodd  12176  qnumval  12185  qdenval  12186  xpnnen  12395  ennnfonelemhdmp1  12410  ennnfonelemss  12411  ennnfonelemnn0  12423  qnnen  12432  ctiunctal  12442  unct  12443  structcnvcnv  12478  setsslid  12513  xpsfrn  12769  xpsff1o2  12770  ringn0  13237  rmodislmodlem  13440  cnfldsub  13472  cnsubmlem  13475  cnsubglem  13476  zring0  13493  tgrest  13672  lmbr2  13717  cnptoprest  13742  lmff  13752  tx1cn  13772  tx2cn  13773  cnblcld  14038  tgioo  14049  reeff1o  14197  pilem1  14203  efhalfpi  14223  coseq0negpitopi  14260  012of  14748  pw1nct  14755  iswomninnlem  14800