ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exlimi Unicode version

Theorem exlimi 1556
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
exlimi.1  |-  F/ x ps
exlimi.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
exlimi  |-  ( E. x ph  ->  ps )

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3  |-  F/ x ps
21nfri 1482 . 2  |-  ( ps 
->  A. x ps )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3exlimih 1555 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1419   E.wex 1451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1408  ax-ie2 1453  ax-4 1470
This theorem depends on definitions:  df-bi 116  df-nf 1420
This theorem is referenced by:  19.36i  1633  euexex  2060  ceqsex  2696  sbhypf  2707  vtoclgf  2716  vtoclg1f  2717  vtoclef  2731  copsexg  4134  copsex2g  4136  ralxpf  4653  rexxpf  4654  dmcoss  4776  fv3  5410  tz6.12c  5417  0neqopab  5782  cnvoprab  6097  bj-exlimmpi  12811
  Copyright terms: Public domain W3C validator