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

Theorem mp2 16
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
Hypotheses
Ref Expression
mp2.1  |-  ph
mp2.2  |-  ps
mp2.3  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mp2  |-  ch

Proof of Theorem mp2
StepHypRef Expression
1 mp2.1 . 2  |-  ph
2 mp2.2 . . 3  |-  ps
3 mp2.3 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mpi 15 . 2  |-  ( ph  ->  ch )
51, 4ax-mp 7 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  impbii  121  pm3.2i  261  sstri  2982  0disj  3789  disjx0  3791  ontr2exmid  4278  0elsucexmid  4317  relres  4667  cnvdif  4758  funopab4  4965  fun0  4985  fvsn  5386  reltpos  5896  tpostpos  5910  tpos0  5920  swoer  6165  xpiderm  6208  erinxp  6211  diffitest  6375  ltrel  7140  lerel  7142  frecfzennn  9367
  Copyright terms: Public domain W3C validator