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  2808  2ordpr  4439  regexmid  4450  ordsoexmid  4477  reg3exmid  4494  intasym  4923  relcoi1  5070  funres11  5195  cnvresid  5197  mpofvex  6101  df1st2  6116  df2nd2  6117  dftpos4  6160  tposf12  6166  frecabcl  6296  xp01disjl  6331  xpcomco  6720  ominf  6790  sbthlem2  6846  djuunr  6951  eldju  6953  ctssdccl  6996  ctssdclemr  6997  omct  7002  ctssexmid  7024  rec1nq  7203  halfnqq  7218  caucvgsrlemasr  7598  axresscn  7668  0re  7766  gtso  7843  cnegexlem2  7938  uzn0  9341  indstr  9388  dfioo2  9757  fnn0nninf  10210  hashinfuni  10523  hashp1i  10556  cnrecnv  10682  rexanuz  10760  xrmaxiflemcom  11018  climdm  11064  sumsnf  11178  tanvalap  11415  egt2lt3  11486  lcmgcdlem  11758  3prm  11809  sqpweven  11853  2sqpwodd  11854  qnumval  11863  qdenval  11864  xpnnen  11907  ennnfonelemhdmp1  11922  ennnfonelemss  11923  ennnfonelemnn0  11935  qnnen  11944  unct  11954  structcnvcnv  11975  setsslid  12009  tgrest  12338  lmbr2  12383  cnptoprest  12408  lmff  12418  tx1cn  12438  tx2cn  12439  cnblcld  12704  tgioo  12715  pilem1  12860  efhalfpi  12880  coseq0negpitopi  12917  isomninnlem  13225