Theorem exlimi 1592

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 1517	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		exlimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	exlimih 1591	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1458  ∃wex 1490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1447  ax-ie2 1492  ax-4 1508

This theorem depends on definitions:  df-bi 117  df-nf 1459

This theorem is referenced by:  19.36i  1670  cbvexv1  1750  euexex  2109  ceqsex  2773  sbhypf  2784  vtoclgf  2793  vtoclg1f  2794  vtoclef  2808  copsexg  4238  copsex2g  4240  ralxpf  4766  rexxpf  4767  dmcoss  4889  fv3  5530  tz6.12c  5537  0neqopab  5910  cnvoprab  6225  bj-exlimmpi  14062