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  4671  regexmid  4682  ordsoexmid  4709  reg3exmid  4727  intasym  5172  relcoi1  5319  funres11  5453  cnvresid  5455  mpofvex  6441  df1st2  6455  df2nd2  6456  dftpos4  6534  tposf12  6540  frecabcl  6670  xp01disjl  6707  xpcomco  7124  1ndom2  7166  ominf  7200  sbthlem2  7275  djuunr  7406  eldju  7408  ctssdccl  7451  ctssdclemr  7452  omct  7457  ctssexmid  7490  rec1nq  7762  halfnqq  7777  caucvgsrlemasr  8157  axresscn  8227  0re  8326  gtso  8404  cnegexlem2  8502  uzn0  9940  indstr  9995  dfioo2  10378  fnn0nninf  10877  hashinfuni  11218  hashp1i  11253  cnrecnv  11678  rexanuz  11756  xrmaxiflemcom  12017  climdm  12063  sumsnf  12178  tanvalap  12477  egt2lt3  12549  lcmgcdlem  12857  3prm  12908  sqpweven  12955  2sqpwodd  12956  qnumval  12965  qdenval  12966  modxai  13197  xpnnen  13287  ennnfonelemhdmp1  13302  ennnfonelemss  13303  ennnfonelemnn0  13315  qnnen  13324  ctiunctal  13334  unct  13335  structcnvcnv  13370  setsslid  13405  prdsvallem  13623  xpsfrn  13673  xpsff1o2  13674  prdsval  14175  ringn0  14367  rmodislmodlem  14689  cnfldstr  14897  cnfldadd  14901  cnfldmul  14903  cnfldsub  14914  cnsubmlem  14917  cnsubglem  14918  zring0  14937  tgrest  15272  lmbr2  15317  cnptoprest  15342  lmff  15352  tx1cn  15372  tx2cn  15373  cnblcld  15638  cnfldms  15639  cnfldtopn  15642  tgioo  15657  reeff1o  15876  pilem1  15883  efhalfpi  15903  coseq0negpitopi  15940  konigsberglem2  16742  konigsberglem5  16745  pw1ninf  17033  012of  17035  pw1nct  17045  rabid1o  17046  stnot  17051  nnnninfen  17076  iswomninnlem  17111