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

Step	Hyp	Ref	Expression
1		exlimi.1	. . 3 ⊢ Ⅎ𝑥𝜓
2	1	nfri 1530	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		exlimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	exlimih 1604	1 ⊢ (∃𝑥𝜑 → 𝜓)

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  2809  vtoclgf  2818  vtoclg1f  2819  vtoclef  2833  copsexg  4273  copsex2g  4275  ralxpf  4808  rexxpf  4809  dmcoss  4931  fv3  5577  tz6.12c  5584  0neqopab  5963  cnvoprab  6287  bj-exlimmpi  15262