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

Theorem exlimi 1526
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 1453 . 2  |-  ( ps 
->  A. x ps )
3 exlimi.2 . 2  |-  ( ph  ->  ps )
42, 3exlimih 1525 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1390   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-4 1441
This theorem depends on definitions:  df-bi 115  df-nf 1391
This theorem is referenced by:  19.36i  1603  euexex  2028  ceqsex  2646  sbhypf  2657  vtoclgf  2666  vtoclef  2680  copsexg  4027  copsex2g  4029  ralxpf  4530  rexxpf  4531  dmcoss  4649  fv3  5250  tz6.12c  5256  0neqopab  5602  cnvoprab  5907  bj-exlimmpi  10859
  Copyright terms: Public domain W3C validator