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  2812  2ordpr  4447  regexmid  4458  ordsoexmid  4485  reg3exmid  4502  intasym  4931  relcoi1  5078  funres11  5203  cnvresid  5205  mpofvex  6109  df1st2  6124  df2nd2  6125  dftpos4  6168  tposf12  6174  frecabcl  6304  xp01disjl  6339  xpcomco  6728  ominf  6798  sbthlem2  6854  djuunr  6959  eldju  6961  ctssdccl  7004  ctssdclemr  7005  omct  7010  ctssexmid  7032  rec1nq  7227  halfnqq  7242  caucvgsrlemasr  7622  axresscn  7692  0re  7790  gtso  7867  cnegexlem2  7962  uzn0  9365  indstr  9415  dfioo2  9787  fnn0nninf  10241  hashinfuni  10555  hashp1i  10588  cnrecnv  10714  rexanuz  10792  xrmaxiflemcom  11050  climdm  11096  sumsnf  11210  tanvalap  11451  egt2lt3  11522  lcmgcdlem  11794  3prm  11845  sqpweven  11889  2sqpwodd  11890  qnumval  11899  qdenval  11900  xpnnen  11943  ennnfonelemhdmp1  11958  ennnfonelemss  11959  ennnfonelemnn0  11971  qnnen  11980  ctiunctal  11990  unct  11991  structcnvcnv  12014  setsslid  12048  tgrest  12377  lmbr2  12422  cnptoprest  12447  lmff  12457  tx1cn  12477  tx2cn  12478  cnblcld  12743  tgioo  12754  reeff1o  12902  pilem1  12908  efhalfpi  12928  coseq0negpitopi  12965  012of  13363  pw1nct  13371  iswomninnlem  13417