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

Theorem exlimi 1605
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
exlimi.1 𝑥𝜓
exlimi.2 (𝜑𝜓)
Assertion
Ref Expression
exlimi (∃𝑥𝜑𝜓)

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3 𝑥𝜓
21nfri 1530 . 2 (𝜓 → ∀𝑥𝜓)
3 exlimi.2 . 2 (𝜑𝜓)
42, 3exlimih 1604 1 (∃𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wnf 1471  wex 1503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1460  ax-ie2 1505  ax-4 1521
This theorem depends on definitions:  df-bi 117  df-nf 1472
This theorem is referenced by:  19.36i  1683  cbvexv1  1763  euexex  2127  ceqsex  2798  sbhypf  2810  vtoclgf  2819  vtoclg1f  2820  vtoclef  2834  copsexg  4274  copsex2g  4276  ralxpf  4809  rexxpf  4810  dmcoss  4932  fv3  5578  tz6.12c  5585  0neqopab  5964  cnvoprab  6289  bj-exlimmpi  15332
  Copyright terms: Public domain W3C validator