Theorem exlimi 2210

Description: Inference associated with 19.23 2204. See exlimiv 1925 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised 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	19.23 2204	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
3		exlimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	mpgbi 1793	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1774  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-12 2170

This theorem depends on definitions:  df-bi 209  df-ex 1775  df-nf 1779

This theorem is referenced by:  equs5av  2273  exlimih  2291  equs5aALT  2378  equs5eALT  2379  equsex  2434  exdistrf  2463  equs5a  2474  equs5e  2475  dfmoeu  2612  moanim  2699  euan  2700  moexexlem  2705  2eu6  2738  ceqsex  3539  sbhypf  3551  vtoclgf  3564  vtoclg1f  3565  vtoclef  3581  rspn0  4311  reusv2lem1  5289  copsexgw  5372  copsexg  5373  copsex2g  5375  rexopabb  5406  0nelopab  5443  ralxpf  5710  dmcoss  5835  fv3  6681  opabiota  6739  oprabidw  7179  zfregcl  9050  scottex  9306  scott0  9307  dfac5lem5  9545  zfcndpow  10030  zfcndreg  10031  zfcndinf  10032  reclem2pr  10462  mreiincl  16859  brabgaf  30351  cnvoprabOLD  30448  bnj607  32181  bnj900  32194  exisym1  33765  exlimii  34147  bj-exlimmpi  34221  bj-exlimmpbi  34222  bj-exlimmpbir  34223  dihglblem5  38426  eu2ndop1stv  43314