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

Theorem exlimi 1528
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 1455 . 2 (𝜓 → ∀𝑥𝜓)
3 exlimi.2 . 2 (𝜑𝜓)
42, 3exlimih 1527 1 (∃𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wnf 1392  wex 1424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1381  ax-ie2 1426  ax-4 1443
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  19.36i  1605  euexex  2030  ceqsex  2651  sbhypf  2662  vtoclgf  2671  vtoclef  2685  copsexg  4045  copsex2g  4047  ralxpf  4550  rexxpf  4551  dmcoss  4670  fv3  5291  tz6.12c  5297  0neqopab  5651  cnvoprab  5956  bj-exlimmpi  11116
  Copyright terms: Public domain W3C validator