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 ⊢ (∃𝑥𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1513  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-4 1563

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

This theorem is used by:  19.36i  1724  cbvexv1  1805  euexex  2172  ceqsex  2860  sbhypf  2872  vtoclgf  2881  vtoclg1f  2882  vtoclef  2898  copsexg  4384  copsex2g  4386  ralxpf  4926  rexxpf  4927  dmcoss  5052  fv3  5718  tz6.12c  5725  0neqopab  6133  cnvoprab  6470  bj-exlimmpi  16798