Theorem exlimi 2211

Description: Inference associated with 19.23 2205. See exlimiv 1934 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 2205	. 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 1914  ax-6 1972  ax-7 2012  ax-12 2172

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

This theorem is referenced by:  sbalex  2236  equsexv  2260  equs5av  2271  exlimih  2286  equs5aALT  2364  equs5eALT  2365  equsex  2418  exdistrf  2447  equs5a  2457  equs5e  2458  dfmoeu  2531  moanim  2617  euan  2618  moexexlem  2623  2eu6  2653  ceqsexOLD  3525  sbhypfOLD  3540  vtoclef  3547  vtoclgf  3555  vtoclg1f  3556  rspn0OLD  4353  reusv2lem1  5396  copsexgw  5490  copsexg  5491  copsex2gOLD  5494  rexopabb  5528  0nelopabOLD  5568  ralxpf  5845  dmcoss  5969  fv3  6907  opabiota  6972  oprabidw  7437  zfregcl  9586  scottex  9877  scott0  9878  dfac5lem5  10119  zfcndpow  10608  zfcndreg  10609  zfcndinf  10610  reclem2pr  11040  mreiincl  17537  brabgaf  31825  cnvoprabOLD  31933  bnj607  33916  bnj900  33929  exisym1  35298  exlimii  35698  bj-exlimmpi  35781  bj-exlimmpbi  35782  bj-exlimmpbir  35783  dihglblem5  40158  tworepnotupword  45587  eu2ndop1stv  45820  pgind  47716