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 ⊢ 𝜒

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  eqvinc  2949  2ordpr  4673  regexmid  4684  ordsoexmid  4711  reg3exmid  4729  intasym  5175  relcoi1  5322  funres11  5456  cnvresid  5458  mpofvex  6445  df1st2  6459  df2nd2  6460  dftpos4  6538  tposf12  6544  frecabcl  6674  xp01disjl  6711  xpcomco  7129  1ndom2  7171  ominf  7205  sbthlem2  7281  djuunr  7413  eldju  7415  ctssdccl  7458  ctssdclemr  7459  omct  7464  ctssexmid  7497  rec1nq  7769  halfnqq  7784  caucvgsrlemasr  8164  axresscn  8234  0re  8333  gtso  8411  cnegexlem2  8510  uzn0  9955  indstr  10010  dfioo2  10394  fnn0nninf  10897  hashinfuni  11239  hashp1i  11274  cnrecnv  11699  rexanuz  11777  xrmaxiflemcom  12041  climdm  12087  sumsnf  12202  tanvalap  12501  egt2lt3  12573  lcmgcdlem  12881  3prm  12932  oddpwdc  12980  sqpweven  12981  2sqpwodd  12982  qnumval  12991  qdenval  12992  modxai  13225  xpnnen  13344  ennnfonelemhdmp1  13359  ennnfonelemss  13360  ennnfonelemnn0  13372  qnnen  13381  ctiunctal  13391  unct  13392  structcnvcnv  13427  setsslid  13462  prdsvallem  13681  xpsfrn  13731  xpsff1o2  13732  gsum2dfilem2  14273  prdsval  14281  ringn0  14473  rmodislmodlem  14797  cnfldstr  15005  cnfldadd  15009  cnfldmul  15011  cnfldsub  15022  cnsubmlem  15025  cnsubglem  15026  zring0  15045  tgrest  15407  lmbr2  15452  cnptoprest  15477  lmff  15487  tx1cn  15507  tx2cn  15508  cnblcld  15773  cnfldms  15774  cnfldtopn  15777  tgioo  15792  reeff1o  16011  pilem1  16018  efhalfpi  16038  coseq0negpitopi  16075  ppiqltx  16293  bposlem6  16328  bposlem8  16330  konigsberglem2  16947  konigsberglem5  16950  pw1ninf  17238  012of  17240  pw1nct  17250  rabid1o  17251  stnot  17256  nnnninfen  17282  iswomninnlem  17318