ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpi Structured version   GIF version

Theorem mpi 15
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 9 . 2 (φψ)
3 mpi.2 . 2 (φ → (ψχ))
42, 3mpd 13 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:  mp2  16  syl6mpi  58  mp2ani  408  pm2.24i  553  simplimdc  756  mp3an3  1220  3impexpbicom  1324  mpisyl  1332  equcomi  1589  equsex  1613  equsexd  1614  spimt  1621  spimeh  1624  equvini  1638  equveli  1639  sbcof2  1688  dveeq2  1693  ax11v2  1698  ax16i  1735  pm13.183  2675  euxfr2dc  2720  sbcth  2771  sbcth2  2839  ssun3  3102  ssun4  3103  ralf0  3318  rext  3942  exss  3954  uniopel  3984  onsucelsucexmid  4215  suc11g  4235  eunex  4239  ordsoexmid  4240  tfisi  4253  finds1  4268  relop  4429  dmrnssfld  4538  iss  4597  relcoi1  4792  nfunv  4876  funimass2  4920  fvssunirng  5133  fvmptg  5191  oprabidlem  5479  fovcl  5548  elovmpt2  5643  tfrlem1  5864  oaword1  5989  nlt1pig  6325  dmaddpq  6363  dmmulpq  6364  archnqq  6400  prarloclemarch2  6402  prarloclemlt  6475  cnegex  6946  nnge1  7678  zneo  8075  bdop  9264  bj-nntrans  9339
  Copyright terms: Public domain W3C validator