Theorem exlimi 2215

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

Syntax hints:   → wi 4  ∃wex 1776  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781

This theorem is referenced by:  sbalexOLD  2241  equsexv  2266  equs5av  2275  exlimih  2288  equs5aALT  2367  equs5eALT  2368  equsex  2421  exdistrf  2450  equs5a  2460  equs5e  2461  dfmoeu  2534  moanim  2618  euan  2619  moexexlem  2624  2eu6  2655  ceqsexOLD  3529  sbhypfOLD  3545  vtoclef  3563  vtoclgf  3569  vtoclg1f  3570  reusv2lem1  5404  copsexgw  5501  copsexg  5502  rexopabb  5538  ralxpf  5860  dmcoss  5988  fv3  6925  opabiota  6991  oprabidw  7462  zfregcl  9632  scottex  9923  scott0  9924  dfac5lem5  10165  zfcndpow  10654  zfcndreg  10655  zfcndinf  10656  reclem2pr  11086  mreiincl  17641  brabgaf  32628  cnvoprabOLD  32738  bnj607  34909  bnj900  34922  exisym1  36407  exlimii  36814  bj-exlimmpi  36895  bj-exlimmpbi  36896  bj-exlimmpbir  36897  dihglblem5  41281  tworepnotupword  46840  eu2ndop1stv  47075  pgind  48948