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 7 . 2  |-  ps
4 mp2b.3 . 2  |-  ( ps 
->  ch )
53, 4ax-mp 7 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 7
This theorem is referenced by:  eqvinc  2667  2ordpr  4249  regexmid  4260  ordsoexmid  4286  reg3exmid  4304  intasym  4709  relcoi1  4849  funres11  4971  cnvresid  4973  mpt2fvex  5829  df1st2  5840  df2nd2  5841  dftpos4  5878  tposf12  5884  xpcomco  6300  rec1nq  6493  halfnqq  6508  caucvgsrlemasr  6874  axresscn  6936  0re  7027  gtso  7097  cnegexlem2  7187  uzn0  8488  indstr  8536  dfioo2  8843  cnrecnv  9510  rexanuz  9587  climdm  9816
  Copyright terms: Public domain W3C validator