Theorem exlimi 1526

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

Syntax hints:   → wi 4  Ⅎwnf 1390  ∃wex 1422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-4 1441

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

This theorem is referenced by:  19.36i  1603  euexex  2027  ceqsex  2638  sbhypf  2649  vtoclgf  2658  vtoclef  2672  copsexg  4007  copsex2g  4009  ralxpf  4510  rexxpf  4511  dmcoss  4629  fv3  5229  tz6.12c  5235  0neqopab  5581  cnvoprab  5886  bj-exlimmpi  10732