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  2719  2ordpr  4275  regexmid  4286  ordsoexmid  4313  reg3exmid  4330  intasym  4739  relcoi1  4879  funres11  5002  cnvresid  5004  mpt2fvex  5860  df1st2  5871  df2nd2  5872  dftpos4  5912  tposf12  5918  frecabcl  6048  xpcomco  6370  ominf  6430  rec1nq  6647  halfnqq  6662  caucvgsrlemasr  7028  axresscn  7090  0re  7181  gtso  7257  cnegexlem2  7351  uzn0  8715  indstr  8762  dfioo2  9073  sizeinfuni  9801  sizep1i  9834  cnrecnv  9935  rexanuz  10012  climdm  10272  lcmgcdlem  10603  3prm  10654  sqpweven  10697  2sqpwodd  10698  xpnnen  10705
  Copyright terms: Public domain W3C validator