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  2949  2ordpr  4669  regexmid  4680  ordsoexmid  4707  reg3exmid  4725  intasym  5170  relcoi1  5317  funres11  5451  cnvresid  5453  mpofvex  6435  df1st2  6449  df2nd2  6450  dftpos4  6528  tposf12  6534  frecabcl  6664  xp01disjl  6701  xpcomco  7118  1ndom2  7160  ominf  7194  sbthlem2  7269  djuunr  7400  eldju  7402  ctssdccl  7445  ctssdclemr  7446  omct  7451  ctssexmid  7484  rec1nq  7756  halfnqq  7771  caucvgsrlemasr  8151  axresscn  8221  0re  8320  gtso  8398  cnegexlem2  8496  uzn0  9921  indstr  9976  dfioo2  10359  fnn0nninf  10858  hashinfuni  11199  hashp1i  11234  cnrecnv  11659  rexanuz  11737  xrmaxiflemcom  11998  climdm  12044  sumsnf  12159  tanvalap  12458  egt2lt3  12530  lcmgcdlem  12838  3prm  12889  sqpweven  12936  2sqpwodd  12937  qnumval  12946  qdenval  12947  modxai  13178  xpnnen  13268  ennnfonelemhdmp1  13283  ennnfonelemss  13284  ennnfonelemnn0  13296  qnnen  13305  ctiunctal  13315  unct  13316  structcnvcnv  13351  setsslid  13386  prdsvallem  13604  xpsfrn  13654  xpsff1o2  13655  prdsval  14156  ringn0  14348  rmodislmodlem  14670  cnfldstr  14878  cnfldadd  14882  cnfldmul  14884  cnfldsub  14895  cnsubmlem  14898  cnsubglem  14899  zring0  14918  tgrest  15253  lmbr2  15298  cnptoprest  15323  lmff  15333  tx1cn  15353  tx2cn  15354  cnblcld  15619  cnfldms  15620  cnfldtopn  15623  tgioo  15638  reeff1o  15857  pilem1  15863  efhalfpi  15883  coseq0negpitopi  15920  konigsberglem2  16713  konigsberglem5  16716  pw1ninf  17004  012of  17006  pw1nct  17016  nnnninfen  17038  iswomninnlem  17073