Theorem exlimi 1647

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

Syntax hints:   → wi 4  Ⅎwnf 1513  ∃wex 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-4 1563

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

This theorem is referenced by:  19.36i  1724  cbvexv1  1805  euexex  2172  ceqsex  2860  sbhypf  2872  vtoclgf  2881  vtoclg1f  2882  vtoclef  2898  copsexg  4379  copsex2g  4381  ralxpf  4921  rexxpf  4922  dmcoss  5047  fv3  5713  tz6.12c  5720  0neqopab  6123  cnvoprab  6460  bj-exlimmpi  16712