Theorem exlimi 2210

Description: Inference associated with 19.23 2204. See exlimiv 1933 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 1801	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1782  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  sbalex  2235  equsexv  2260  equs5av  2271  exlimih  2286  equs5aALT  2364  equs5eALT  2365  equsex  2418  exdistrf  2447  equs5a  2457  equs5e  2458  dfmoeu  2536  moanim  2622  euan  2623  moexexlem  2628  2eu6  2658  ceqsex  3477  sbhypf  3490  vtoclgf  3502  vtoclg1f  3503  vtoclef  3522  rspn0OLD  4289  reusv2lem1  5323  copsexgw  5406  copsexg  5407  copsex2gOLD  5410  rexopabb  5443  0nelopabOLD  5483  ralxpf  5757  dmcoss  5882  fv3  6794  opabiota  6853  oprabidw  7308  zfregcl  9351  scottex  9641  scott0  9642  dfac5lem5  9881  zfcndpow  10370  zfcndreg  10371  zfcndinf  10372  reclem2pr  10802  mreiincl  17303  brabgaf  30945  cnvoprabOLD  31052  bnj607  32893  bnj900  32906  exisym1  34610  exlimii  35011  bj-exlimmpi  35094  bj-exlimmpbi  35095  bj-exlimmpbir  35096  dihglblem5  39309  eu2ndop1stv  44584  tworepnotupword  46488