Theorem exlimi 1640

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

Syntax hints:   → wi 4  Ⅎwnf 1506  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-4 1556

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

This theorem is referenced by:  19.36i  1718  cbvexv1  1798  euexex  2163  ceqsex  2839  sbhypf  2851  vtoclgf  2860  vtoclg1f  2861  vtoclef  2877  copsexg  4334  copsex2g  4336  ralxpf  4874  rexxpf  4875  dmcoss  5000  fv3  5658  tz6.12c  5665  0neqopab  6061  cnvoprab  6394  bj-exlimmpi  16302