ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp2b Unicode version

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
StepHypRef Expression
1 mp2b.1 . . 3  |-  ph
2 mp2b.2 . . 3  |-  ( ph  ->  ps )
31, 2ax-mp 5 . 2  |-  ps
4 mp2b.3 . 2  |-  ( ps 
->  ch )
53, 4ax-mp 5 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5
This theorem is referenced by:  eqvinc  2811  2ordpr  4446  regexmid  4457  ordsoexmid  4484  reg3exmid  4501  intasym  4930  relcoi1  5077  funres11  5202  cnvresid  5204  mpofvex  6108  df1st2  6123  df2nd2  6124  dftpos4  6167  tposf12  6173  frecabcl  6303  xp01disjl  6338  xpcomco  6727  ominf  6797  sbthlem2  6853  djuunr  6958  eldju  6960  ctssdccl  7003  ctssdclemr  7004  omct  7009  ctssexmid  7031  rec1nq  7226  halfnqq  7241  caucvgsrlemasr  7621  axresscn  7691  0re  7789  gtso  7866  cnegexlem2  7961  uzn0  9364  indstr  9414  dfioo2  9786  fnn0nninf  10240  hashinfuni  10554  hashp1i  10587  cnrecnv  10713  rexanuz  10791  xrmaxiflemcom  11049  climdm  11095  sumsnf  11209  tanvalap  11449  egt2lt3  11520  lcmgcdlem  11792  3prm  11843  sqpweven  11887  2sqpwodd  11888  qnumval  11897  qdenval  11898  xpnnen  11941  ennnfonelemhdmp1  11956  ennnfonelemss  11957  ennnfonelemnn0  11969  qnnen  11978  ctiunctal  11988  unct  11989  structcnvcnv  12012  setsslid  12046  tgrest  12375  lmbr2  12420  cnptoprest  12445  lmff  12455  tx1cn  12475  tx2cn  12476  cnblcld  12741  tgioo  12752  reeff1o  12900  pilem1  12906  efhalfpi  12926  coseq0negpitopi  12963  012of  13361  pw1nct  13369  iswomninnlem  13415
  Copyright terms: Public domain W3C validator