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