Theorem exlimi 1643

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

Syntax hints:   → wi 4  Ⅎwnf 1509  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-4 1559

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

This theorem is referenced by:  19.36i  1720  cbvexv1  1801  euexex  2168  ceqsex  2854  sbhypf  2866  vtoclgf  2875  vtoclg1f  2876  vtoclef  2892  copsexg  4365  copsex2g  4367  ralxpf  4906  rexxpf  4907  dmcoss  5032  fv3  5698  tz6.12c  5705  0neqopab  6106  cnvoprab  6443  bj-exlimmpi  16668