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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  mp2  16  syl6mpi  58  mp2ani  408  pm2.24i  553  simplimdc  757  mp3an3  1221  3impexpbicom  1327  mpisyl  1335  equcomi  1592  equsex  1616  equsexd  1617  spimt  1624  spimeh  1627  equvini  1641  equveli  1642  sbcof2  1691  dveeq2  1696  ax11v2  1701  ax16i  1738  pm13.183  2681  euxfr2dc  2726  sbcth  2777  sbcth2  2845  ssun3  3108  ssun4  3109  ralf0  3324  rext  3951  exss  3963  uniopel  3993  onsucelsucexmid  4255  suc11g  4281  eunex  4285  ordsoexmid  4286  tfisi  4310  finds1  4325  relop  4486  dmrnssfld  4595  iss  4654  relcoi1  4849  nfunv  4933  funimass2  4977  fvssunirng  5190  fvmptg  5248  oprabidlem  5536  fovcl  5606  elovmpt2  5701  tfrlem1  5923  oaword1  6050  diffifi  6351  nlt1pig  6437  dmaddpq  6475  dmmulpq  6476  archnqq  6513  prarloclemarch2  6515  prarloclemlt  6589  cnegex  7187  nnge1  7935  zneo  8337  bdop  9969  bj-nntrans  10050
  Copyright terms: Public domain W3C validator