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  2887  2ordpr  4561  regexmid  4572  ordsoexmid  4599  reg3exmid  4617  intasym  5055  relcoi1  5202  funres11  5331  cnvresid  5333  mpofvex  6272  df1st2  6286  df2nd2  6287  dftpos4  6330  tposf12  6336  frecabcl  6466  xp01disjl  6501  xpcomco  6894  ominf  6966  sbthlem2  7033  djuunr  7141  eldju  7143  ctssdccl  7186  ctssdclemr  7187  omct  7192  ctssexmid  7225  rec1nq  7479  halfnqq  7494  caucvgsrlemasr  7874  axresscn  7944  0re  8043  gtso  8122  cnegexlem2  8219  uzn0  9634  indstr  9684  dfioo2  10066  fnn0nninf  10547  hashinfuni  10886  hashp1i  10919  cnrecnv  11092  rexanuz  11170  xrmaxiflemcom  11431  climdm  11477  sumsnf  11591  tanvalap  11890  egt2lt3  11962  lcmgcdlem  12270  3prm  12321  sqpweven  12368  2sqpwodd  12369  qnumval  12378  qdenval  12379  modxai  12610  xpnnen  12636  ennnfonelemhdmp1  12651  ennnfonelemss  12652  ennnfonelemnn0  12664  qnnen  12673  ctiunctal  12683  unct  12684  structcnvcnv  12719  setsslid  12754  prdsvallem  12974  prdsval  12975  xpsfrn  13052  xpsff1o2  13053  ringn0  13692  rmodislmodlem  13982  cnfldstr  14190  cnfldadd  14194  cnfldmul  14196  cnfldsub  14207  cnsubmlem  14210  cnsubglem  14211  zring0  14232  tgrest  14489  lmbr2  14534  cnptoprest  14559  lmff  14569  tx1cn  14589  tx2cn  14590  cnblcld  14855  cnfldms  14856  cnfldtopn  14859  tgioo  14874  reeff1o  15093  pilem1  15099  efhalfpi  15119  coseq0negpitopi  15156  012of  15724  pw1nct  15734  nnnninfen  15752  iswomninnlem  15780