NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpi Unicode version

Theorem mpi 16
Description: A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypotheses
Ref Expression
mpi.1
mpi.2
Assertion
Ref Expression
mpi

Proof of Theorem mpi
StepHypRef Expression
1 mpi.1 . . 3
21a1i 10 . 2
3 mpi.2 . 2
42, 3mpd 14 1
Colors of variables: wff setvar class
Syntax hints:   wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mp2  17  syl6mpi  58  mp2ani  659  mp3an3  1266  3impexpbicom  1367  ee10  1376  merco2  1501  equcomi  1679  ax10  1944  equveli  1988  ax11v2  1992  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  pm13.183  2979  sbcth  3060  sbcth2  3129  ssun3  3428  ssun4  3429  uneqdifeq  3638  ralf0  3656  uniintsn  3963  opkth1g  4130  funimass2  5170  fvopab4g  5388  fovcl  5588  ov2ag  5598  ov3  5599  fnfreclem3  6319
  Copyright terms: Public domain W3C validator