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  4354  reusv2lem1  5397  copsexgw  5491  copsexg  5492  copsex2gOLD  5495  rexopabb  5529  0nelopabOLD  5569  ralxpf  5847  dmcoss  5971  fv3  6910  opabiota  6975  oprabidw  7440  zfregcl  9589  scottex  9880  scott0  9881  dfac5lem5  10122  zfcndpow  10611  zfcndreg  10612  zfcndinf  10613  reclem2pr  11043  mreiincl  17540  brabgaf  31837  cnvoprabOLD  31945  bnj607  33927  bnj900  33940  exisym1  35309  exlimii  35709  bj-exlimmpi  35792  bj-exlimmpbi  35793  bj-exlimmpbir  35794  dihglblem5  40169  tworepnotupword  45600  eu2ndop1stv  45833  pgind  47762