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  410  mpanr2OLD  417  pm2.24i  541  simplimdc  750  mp3an3  1206  3impexpbicom  1306  ee10  1314  equcomi  1574  equsex  1598  equsexd  1599  spimt  1606  spimeh  1609  equvini  1623  equveli  1624  sbcof2  1673  dveeq2  1678  ax11v2  1683  ax16i  1720  pm13.183  2658  euxfr2dc  2703  sbcth  2754  sbcth2  2822  ssun3  3085  ssun4  3086  ralf0  3303  rext  3925  exss  3937  uniopel  3967  onsucelsucexmid  4199  suc11g  4219  eunex  4223  ordsoexmid  4224  tfisi  4237  finds1  4252  relop  4413  dmrnssfld  4522  iss  4581  relcoi1  4776  nfunv  4859  funimass2  4903  fvssunirng  5115  fvmptg  5173  oprabidlem  5460  fovcl  5529  elovmpt2  5624  tfrlem1  5845  oaword1  5965  nlt1pig  6201  dmaddpq  6238  dmmulpq  6239  archnqq  6274  prarloclemarch2  6276  prarloclemlt  6347  cnegex  6776  bdop  7102  bj-nntrans  7173
  Copyright terms: Public domain W3C validator