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

Theorem exlimi 1558
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 1484 . 2 (𝜓 → ∀𝑥𝜓)
3 exlimi.2 . 2 (𝜑𝜓)
42, 3exlimih 1557 1 (∃𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wnf 1421  wex 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1410  ax-ie2 1455  ax-4 1472
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  19.36i  1635  euexex  2062  ceqsex  2698  sbhypf  2709  vtoclgf  2718  vtoclg1f  2719  vtoclef  2733  copsexg  4136  copsex2g  4138  ralxpf  4655  rexxpf  4656  dmcoss  4778  fv3  5412  tz6.12c  5419  0neqopab  5784  cnvoprab  6099  bj-exlimmpi  12904
  Copyright terms: Public domain W3C validator