ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exlimi GIF 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 𝑥𝜓
exlimi.2 (𝜑𝜓)
Assertion
Ref Expression
exlimi (∃𝑥𝜑𝜓)

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3 𝑥𝜓
21nfri 1453 . 2 (𝜓 → ∀𝑥𝜓)
3 exlimi.2 . 2 (𝜑𝜓)
42, 3exlimih 1525 1 (∃𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wnf 1390  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  2027  ceqsex  2638  sbhypf  2649  vtoclgf  2658  vtoclef  2672  copsexg  4007  copsex2g  4009  ralxpf  4510  rexxpf  4511  dmcoss  4629  fv3  5229  tz6.12c  5235  0neqopab  5581  cnvoprab  5886  bj-exlimmpi  10732
  Copyright terms: Public domain W3C validator