Theorem exlimi 1541

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

Syntax hints:   → wi 4  Ⅎwnf 1404  ∃wex 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-gen 1393  ax-ie2 1438  ax-4 1455

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

This theorem is referenced by:  19.36i  1618  euexex  2045  ceqsex  2679  sbhypf  2690  vtoclgf  2699  vtoclg1f  2700  vtoclef  2714  copsexg  4104  copsex2g  4106  ralxpf  4623  rexxpf  4624  dmcoss  4744  fv3  5376  tz6.12c  5383  0neqopab  5748  cnvoprab  6061  bj-exlimmpi  12559