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  1800  euexex  2165  ceqsex  2842  sbhypf  2854  vtoclgf  2863  vtoclg1f  2864  vtoclef  2880  copsexg  4342  copsex2g  4344  ralxpf  4882  rexxpf  4883  dmcoss  5008  fv3  5671  tz6.12c  5678  0neqopab  6076  cnvoprab  6408  bj-exlimmpi  16471