Theorem exlimi 1525

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

Syntax hints:   → wi 4  Ⅎwnf 1389  ∃wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1378  ax-ie2 1423  ax-4 1440

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  19.36i  1602  euexex  2026  ceqsex  2637  sbhypf  2648  vtoclgf  2657  vtoclef  2671  copsexg  3999  copsex2g  4001  ralxpf  4500  rexxpf  4501  dmcoss  4619  fv3  5218  tz6.12c  5224  0neqopab  5570  cnvoprab  5875  bj-exlimmpi  10581