Theorem exlimi 2233

Description: Inference associated with 19.23 2227. See exlimiv 2007 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 2227	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
3		exlimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	mpgbi 1874	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1853  Ⅎwnf 1857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196

This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1854  df-nf 1859

This theorem is referenced by:  exlimih  2295  equs5aALT  2322  equs5eALT  2323  equsex  2437  nfeqf2  2442  exdistrf  2473  equs5a  2485  equs5e  2486  mo2v  2614  moanim  2667  euan  2668  moexex  2679  2eu6  2696  ceqsex  3381  sbhypf  3393  vtoclgf  3404  vtoclg1f  3405  vtoclef  3421  rspn0  4077  reusv2lem1  5017  copsexg  5104  copsex2g  5106  ralxpf  5424  dmcoss  5540  fv3  6367  tz6.12c  6374  opabiota  6423  0neqopab  6863  zfregcl  8664  scottex  8921  scott0  8922  dfac5lem5  9140  zfcndpow  9630  zfcndreg  9631  zfcndinf  9632  reclem2pr  10062  mreiincl  16458  brabgaf  29727  cnvoprabOLD  29807  bnj607  31293  bnj900  31306  exisym1  32729  exlimii  33124  bj-exlimmpi  33211  bj-exlimmpbi  33212  bj-exlimmpbir  33213  dihglblem5  37089  eu2ndop1stv  41708