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
mp2.2
mp2.3
Assertion
Ref Expression
mp2

Proof of Theorem mp2
StepHypRef Expression
1 mp2.1 . 2
2 mp2.2 . . 3
3 mp2.3 . . 3
42, 3mpi 15 . 2
51, 4ax-mp 7 1
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  2948  0disj  3752  disjx0  3754  relres  4582  cnvdif  4673  funopab4  4880  fun0  4900  fvsn  5301  reltpos  5806  tpostpos  5820  tpos0  5830  swoer  6070  xpiderm  6113  erinxp  6116  ltrel  6878  lerel  6880  frecfzennn  8884
  Copyright terms: Public domain W3C validator