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

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  7407  eldju  7409  ctssdccl  7452  ctssdclemr  7453  omct  7458  ctssexmid  7491  rec1nq  7763  halfnqq  7778  caucvgsrlemasr  8158  axresscn  8228  0re  8327  gtso  8405  cnegexlem2  8504  uzn0  9948  indstr  10003  dfioo2  10387  fnn0nninf  10890  hashinfuni  11232  hashp1i  11267  cnrecnv  11692  rexanuz  11770  xrmaxiflemcom  12034  climdm  12080  sumsnf  12195  tanvalap  12494  egt2lt3  12566  lcmgcdlem  12874  3prm  12925  oddpwdc  12973  sqpweven  12974  2sqpwodd  12975  qnumval  12984  qdenval  12985  modxai  13218  xpnnen  13337  ennnfonelemhdmp1  13352  ennnfonelemss  13353  ennnfonelemnn0  13365  qnnen  13374  ctiunctal  13384  unct  13385  structcnvcnv  13420  setsslid  13455  prdsvallem  13674  xpsfrn  13724  xpsff1o2  13725  prdsval  14257  ringn0  14449  rmodislmodlem  14771  cnfldstr  14979  cnfldadd  14983  cnfldmul  14985  cnfldsub  14996  cnsubmlem  14999  cnsubglem  15000  zring0  15019  tgrest  15361  lmbr2  15406  cnptoprest  15431  lmff  15441  tx1cn  15461  tx2cn  15462  cnblcld  15727  cnfldms  15728  cnfldtopn  15731  tgioo  15746  reeff1o  15965  pilem1  15972  efhalfpi  15992  coseq0negpitopi  16029  ppiqltx  16242  bposlem6  16277  bposlem8  16279  konigsberglem2  16896  konigsberglem5  16899  pw1ninf  17187  012of  17189  pw1nct  17199  rabid1o  17200  stnot  17205  nnnninfen  17230  iswomninnlem  17266