Theorem exlimi 1642

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

Syntax hints:   → wi 4  Ⅎwnf 1508  ∃wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1497  ax-ie2 1542  ax-4 1558

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

This theorem is referenced by:  19.36i  1720  cbvexv1  1800  euexex  2165  ceqsex  2841  sbhypf  2853  vtoclgf  2862  vtoclg1f  2863  vtoclef  2879  copsexg  4336  copsex2g  4338  ralxpf  4876  rexxpf  4877  dmcoss  5002  fv3  5662  tz6.12c  5669  0neqopab  6065  cnvoprab  6398  bj-exlimmpi  16366