Theorem exlimi 2253

Description: Inference associated with 19.23 2247. See exlimiv 2021 for a version with a dv 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 2247	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
3		exlimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	mpgbi 1880	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1859  Ⅎwnf 1863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-12 2214

This theorem depends on definitions:  df-bi 198  df-or 866  df-ex 1860  df-nf 1864

This theorem is referenced by:  exlimih  2325  equs5aALT  2351  equs5eALT  2352  equsex  2459  nfeqf2OLD  2465  exdistrf  2495  equs5a  2506  equs5e  2507  mo2v  2639  moanim  2693  euan  2694  moexex  2705  2eu6  2722  ceqsex  3435  sbhypf  3447  vtoclgf  3457  vtoclg1f  3458  vtoclef  3474  rspn0  4135  reusv2lem1  5067  copsexg  5145  copsex2g  5147  ralxpf  5470  dmcoss  5586  fv3  6422  opabiota  6478  0neqopab  6924  zfregcl  8734  scottex  8991  scott0  8992  dfac5lem5  9229  zfcndpow  9719  zfcndreg  9720  zfcndinf  9721  reclem2pr  10151  mreiincl  16457  brabgaf  29741  cnvoprabOLD  29821  bnj607  31304  bnj900  31317  exisym1  32735  exlimii  33126  bj-exlimmpi  33209  bj-exlimmpbi  33210  bj-exlimmpbir  33211  dihglblem5  37073  eu2ndop1stv  41708