Theorem mp2b 8

Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)

Hypotheses

Ref	Expression
mp2b.1	|- ph
mp2b.2	|- ( ph -> ps )
mp2b.3	|- ( ps -> ch )

Assertion

Ref	Expression
mp2b	|- ch

Proof of Theorem mp2b

Step	Hyp	Ref	Expression
1		mp2b.1	. . 3 |- ph
2		mp2b.2	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 5	. 2 |- ps
4		mp2b.3	. 2 |- ( ps -> ch )
5	3, 4	ax-mp 5	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  eqvinc  2929  2ordpr  4622  regexmid  4633  ordsoexmid  4660  reg3exmid  4678  intasym  5121  relcoi1  5268  funres11  5402  cnvresid  5404  mpofvex  6369  df1st2  6383  df2nd2  6384  dftpos4  6428  tposf12  6434  frecabcl  6564  xp01disjl  6601  xpcomco  7009  1ndom2  7050  ominf  7084  sbthlem2  7156  djuunr  7264  eldju  7266  ctssdccl  7309  ctssdclemr  7310  omct  7315  ctssexmid  7348  rec1nq  7614  halfnqq  7629  caucvgsrlemasr  8009  axresscn  8079  0re  8178  gtso  8257  cnegexlem2  8354  uzn0  9771  indstr  9826  dfioo2  10208  fnn0nninf  10699  hashinfuni  11038  hashp1i  11073  cnrecnv  11470  rexanuz  11548  xrmaxiflemcom  11809  climdm  11855  sumsnf  11969  tanvalap  12268  egt2lt3  12340  lcmgcdlem  12648  3prm  12699  sqpweven  12746  2sqpwodd  12747  qnumval  12756  qdenval  12757  modxai  12988  xpnnen  13014  ennnfonelemhdmp1  13029  ennnfonelemss  13030  ennnfonelemnn0  13042  qnnen  13051  ctiunctal  13061  unct  13062  structcnvcnv  13097  setsslid  13132  prdsvallem  13354  prdsval  13355  xpsfrn  13432  xpsff1o2  13433  ringn0  14072  rmodislmodlem  14363  cnfldstr  14571  cnfldadd  14575  cnfldmul  14577  cnfldsub  14588  cnsubmlem  14591  cnsubglem  14592  zring0  14613  tgrest  14892  lmbr2  14937  cnptoprest  14962  lmff  14972  tx1cn  14992  tx2cn  14993  cnblcld  15258  cnfldms  15259  cnfldtopn  15262  tgioo  15277  reeff1o  15496  pilem1  15502  efhalfpi  15522  coseq0negpitopi  15559  pw1ninf  16590  012of  16592  pw1nct  16604  nnnninfen  16623  iswomninnlem  16653