ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpi 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-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mp2  16  syl6mpi  64  mp2ani  428  pm2.24i  597  simplimdc  830  mp3an3  1289  3impexpbicom  1399  mpisyl  1407  equcomi  1665  equsex  1691  equsexd  1692  spimt  1699  spimeh  1702  equvini  1716  equveli  1717  sbcof2  1766  dveeq2  1771  ax11v2  1776  ax16i  1814  pm13.183  2796  euxfr2dc  2842  sbcth  2895  sbcth2  2968  ssun3  3211  ssun4  3212  ralf0  3436  exmidexmid  4090  rext  4107  exss  4119  uniopel  4148  onsucelsucexmid  4415  suc11g  4442  eunex  4446  ordsoexmid  4447  tfisi  4471  finds1  4486  omsinds  4505  relop  4659  dmrnssfld  4772  iss  4835  relcoi1  5040  nfunv  5126  funimass2  5171  fvssunirng  5404  fvmptg  5465  oprabidlem  5770  fovcl  5844  elovmpo  5939  tfrlem1  6173  oaword1  6335  0domg  6699  diffifi  6756  exmidpw  6770  djulclb  6908  0ct  6960  nlt1pig  7117  dmaddpq  7155  dmmulpq  7156  archnqq  7193  prarloclemarch2  7195  prarloclemlt  7269  cnegex  7908  nnge1  8711  zneo  9120  fsum2d  11172  fsumabs  11202  fsumiun  11214  efne0  11311  nn0o1gt2  11529  ennnfonelemex  11854  qtopbasss  12617  coseq0negpitopi  12844  cos02pilt1  12859  bdop  13000  bj-nntrans  13076
  Copyright terms: Public domain W3C validator