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  124  pm3.2i  266  sstri  3034  0disj  3842  disjx0  3844  ontr2exmid  4341  0elsucexmid  4381  relres  4741  cnvdif  4838  funopab4  5051  fun0  5072  fvsn  5492  reltpos  6015  tpostpos  6029  tpos0  6039  oawordriexmid  6231  swoer  6318  xpiderm  6361  erinxp  6364  domfiexmid  6592  diffitest  6601  ltrel  7546  lerel  7548  frecfzennn  9829  sum0  10776  pw1dom2  11844
  Copyright terms: Public domain W3C validator