Theorem exlimi 2073

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

Syntax hints:   → wi 4  ∃wex 1695  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-ex 1696  df-nf 1701

This theorem is referenced by:  exlimih  2133  equs5aALT  2165  equs5eALT  2166  equsex  2281  nfeqf2  2285  exdistrf  2321  equs5a  2336  equs5e  2337  mo2v  2465  moanim  2517  euan  2518  moexex  2529  2eu6  2546  ceqsex  3214  sbhypf  3226  vtoclgf  3237  vtoclg1f  3238  vtoclef  3254  rspn0  3892  reusv2lem1  4794  copsexg  4882  copsex2g  4884  ralxpf  5190  dmcoss  5306  fv3  6116  tz6.12c  6123  opabiota  6171  0neqopab  6596  zfregcl  8382  zfregclOLD  8384  scottex  8631  scott0  8632  dfac5lem5  8833  zfcndpow  9317  zfcndreg  9318  zfcndinf  9319  reclem2pr  9749  mreiincl  16079  brabgaf  28800  cnvoprab  28886  bnj607  30240  bnj900  30253  exisym1  31593  exlimii  32006  bj-exlimmpi  32097  bj-exlimmpbi  32098  bj-exlimmpbir  32099  dihglblem5  35605  eu2ndop1stv  39851