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  2942  2ordpr  4648  regexmid  4659  ordsoexmid  4686  reg3exmid  4704  intasym  5149  relcoi1  5296  funres11  5430  cnvresid  5432  mpofvex  6403  df1st2  6417  df2nd2  6418  dftpos4  6496  tposf12  6502  frecabcl  6632  xp01disjl  6669  xpcomco  7079  1ndom2  7121  ominf  7155  sbthlem2  7230  djuunr  7359  eldju  7361  ctssdccl  7404  ctssdclemr  7405  omct  7410  ctssexmid  7443  rec1nq  7715  halfnqq  7730  caucvgsrlemasr  8110  axresscn  8180  0re  8279  gtso  8357  cnegexlem2  8454  uzn0  9876  indstr  9931  dfioo2  10313  fnn0nninf  10807  hashinfuni  11148  hashp1i  11183  cnrecnv  11603  rexanuz  11681  xrmaxiflemcom  11942  climdm  11988  sumsnf  12103  tanvalap  12402  egt2lt3  12474  lcmgcdlem  12782  3prm  12833  sqpweven  12880  2sqpwodd  12881  qnumval  12890  qdenval  12891  modxai  13122  xpnnen  13166  ennnfonelemhdmp1  13181  ennnfonelemss  13182  ennnfonelemnn0  13194  qnnen  13203  ctiunctal  13213  unct  13214  structcnvcnv  13249  setsslid  13284  prdsvallem  13506  prdsval  13507  xpsfrn  13584  xpsff1o2  13585  ringn0  14225  rmodislmodlem  14547  cnfldstr  14755  cnfldadd  14759  cnfldmul  14761  cnfldsub  14772  cnsubmlem  14775  cnsubglem  14776  zring0  14797  tgrest  15083  lmbr2  15128  cnptoprest  15153  lmff  15163  tx1cn  15183  tx2cn  15184  cnblcld  15449  cnfldms  15450  cnfldtopn  15453  tgioo  15468  reeff1o  15687  pilem1  15693  efhalfpi  15713  coseq0negpitopi  15750  konigsberglem2  16533  konigsberglem5  16536  pw1ninf  16814  012of  16816  pw1nct  16826  nnnninfen  16848  iswomninnlem  16883