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  426  pm2.24i  595  simplimdc  828  mp3an3  1287  3impexpbicom  1397  mpisyl  1405  equcomi  1663  equsex  1689  equsexd  1690  spimt  1697  spimeh  1700  equvini  1714  equveli  1715  sbcof2  1764  dveeq2  1769  ax11v2  1774  ax16i  1812  pm13.183  2794  euxfr2dc  2840  sbcth  2893  sbcth2  2966  ssun3  3209  ssun4  3210  ralf0  3434  exmidexmid  4088  rext  4105  exss  4117  uniopel  4146  onsucelsucexmid  4413  suc11g  4440  eunex  4444  ordsoexmid  4445  tfisi  4469  finds1  4484  omsinds  4503  relop  4657  dmrnssfld  4770  iss  4833  relcoi1  5038  nfunv  5124  funimass2  5169  fvssunirng  5402  fvmptg  5463  oprabidlem  5768  fovcl  5842  elovmpo  5937  tfrlem1  6171  oaword1  6333  0domg  6697  diffifi  6754  exmidpw  6768  djulclb  6906  0ct  6958  nlt1pig  7113  dmaddpq  7151  dmmulpq  7152  archnqq  7189  prarloclemarch2  7191  prarloclemlt  7265  cnegex  7904  nnge1  8703  zneo  9106  fsum2d  11155  fsumabs  11185  fsumiun  11197  efne0  11294  nn0o1gt2  11509  ennnfonelemex  11833  qtopbasss  12596  bdop  12907  bj-nntrans  12983
  Copyright terms: Public domain W3C validator