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  2928  2ordpr  4624  regexmid  4635  ordsoexmid  4662  reg3exmid  4680  intasym  5123  relcoi1  5270  funres11  5404  cnvresid  5406  mpofvex  6375  df1st2  6389  df2nd2  6390  dftpos4  6434  tposf12  6440  frecabcl  6570  xp01disjl  6607  xpcomco  7015  1ndom2  7056  ominf  7090  sbthlem2  7162  djuunr  7270  eldju  7272  ctssdccl  7315  ctssdclemr  7316  omct  7321  ctssexmid  7354  rec1nq  7620  halfnqq  7635  caucvgsrlemasr  8015  axresscn  8085  0re  8184  gtso  8263  cnegexlem2  8360  uzn0  9777  indstr  9832  dfioo2  10214  fnn0nninf  10706  hashinfuni  11045  hashp1i  11080  cnrecnv  11493  rexanuz  11571  xrmaxiflemcom  11832  climdm  11878  sumsnf  11993  tanvalap  12292  egt2lt3  12364  lcmgcdlem  12672  3prm  12723  sqpweven  12770  2sqpwodd  12771  qnumval  12780  qdenval  12781  modxai  13012  xpnnen  13038  ennnfonelemhdmp1  13053  ennnfonelemss  13054  ennnfonelemnn0  13066  qnnen  13075  ctiunctal  13085  unct  13086  structcnvcnv  13121  setsslid  13156  prdsvallem  13378  prdsval  13379  xpsfrn  13456  xpsff1o2  13457  ringn0  14097  rmodislmodlem  14388  cnfldstr  14596  cnfldadd  14600  cnfldmul  14602  cnfldsub  14613  cnsubmlem  14616  cnsubglem  14617  zring0  14638  tgrest  14922  lmbr2  14967  cnptoprest  14992  lmff  15002  tx1cn  15022  tx2cn  15023  cnblcld  15288  cnfldms  15289  cnfldtopn  15292  tgioo  15307  reeff1o  15526  pilem1  15532  efhalfpi  15552  coseq0negpitopi  15589  konigsberglem2  16369  konigsberglem5  16372  pw1ninf  16650  012of  16652  pw1nct  16664  nnnninfen  16686  iswomninnlem  16721