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  117  pm3.2i  257  sstri  2954  0disj  3761  disjx0  3763  ontr2exmid  4250  0elsucexmid  4289  relres  4639  cnvdif  4730  funopab4  4937  fun0  4957  fvsn  5358  reltpos  5865  tpostpos  5879  tpos0  5889  swoer  6134  xpiderm  6177  erinxp  6180  diffitest  6344  ltrel  7081  lerel  7083  frecfzennn  9203
  Copyright terms: Public domain W3C validator