Theorem exlimi 1574

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

Syntax hints:   → wi 4  Ⅎwnf 1437  ∃wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1426  ax-ie2 1471  ax-4 1488

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

This theorem is referenced by:  19.36i  1651  euexex  2085  ceqsex  2727  sbhypf  2738  vtoclgf  2747  vtoclg1f  2748  vtoclef  2762  copsexg  4174  copsex2g  4176  ralxpf  4693  rexxpf  4694  dmcoss  4816  fv3  5452  tz6.12c  5459  0neqopab  5824  cnvoprab  6139  bj-exlimmpi  13148