Theorem exlimi 1582

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

Syntax hints:   → wi 4  Ⅎwnf 1448  ∃wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1437  ax-ie2 1482  ax-4 1498

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  19.36i  1660  cbvexv1  1740  euexex  2099  ceqsex  2764  sbhypf  2775  vtoclgf  2784  vtoclg1f  2785  vtoclef  2799  copsexg  4222  copsex2g  4224  ralxpf  4750  rexxpf  4751  dmcoss  4873  fv3  5509  tz6.12c  5516  0neqopab  5887  cnvoprab  6202  bj-exlimmpi  13661