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

Theorem exlimi 1530
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 1457 . 2  |-  ( ps 
->  A. x ps )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3exlimih 1529 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1394   E.wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1383  ax-ie2 1428  ax-4 1445
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  19.36i  1607  euexex  2033  ceqsex  2657  sbhypf  2668  vtoclgf  2677  vtoclg1f  2678  vtoclef  2692  copsexg  4062  copsex2g  4064  ralxpf  4570  rexxpf  4571  dmcoss  4690  fv3  5312  tz6.12c  5318  0neqopab  5676  cnvoprab  5981  bj-exlimmpi  11328
  Copyright terms: Public domain W3C validator