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  63  mp2ani  423  pm2.24i  586  simplimdc  791  mp3an3  1258  3impexpbicom  1368  mpisyl  1376  equcomi  1633  equsex  1657  equsexd  1658  spimt  1665  spimeh  1668  equvini  1682  equveli  1683  sbcof2  1732  dveeq2  1737  ax11v2  1742  ax16i  1780  pm13.183  2733  euxfr2dc  2778  sbcth  2829  sbcth2  2902  ssun3  3138  ssun4  3139  ralf0  3346  rext  3972  exss  3984  uniopel  4013  onsucelsucexmid  4275  suc11g  4302  eunex  4306  ordsoexmid  4307  tfisi  4330  finds1  4345  relop  4508  dmrnssfld  4617  iss  4678  relcoi1  4873  nfunv  4957  funimass2  5002  fvssunirng  5215  fvmptg  5274  oprabidlem  5561  fovcl  5631  elovmpt2  5726  tfrlem1  5951  oaword1  6108  diffifi  6418  nlt1pig  6582  dmaddpq  6620  dmmulpq  6621  archnqq  6658  prarloclemarch2  6660  prarloclemlt  6734  cnegex  7342  nnge1  8118  zneo  8518  nn0o1gt2  10438  bdop  10809  bj-nntrans  10889
  Copyright terms: Public domain W3C validator