Theorem exlimi 2084

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

Syntax hints:   → wi 4  ∃wex 1701  Ⅎwnf 1705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1702  df-nf 1707

This theorem is referenced by:  exlimih  2144  equs5aALT  2176  equs5eALT  2177  equsex  2292  nfeqf2  2296  exdistrf  2332  equs5a  2347  equs5e  2348  mo2v  2476  moanim  2528  euan  2529  moexex  2540  2eu6  2557  ceqsex  3231  sbhypf  3243  vtoclgf  3254  vtoclg1f  3255  vtoclef  3271  rspn0  3916  reusv2lem1  4838  copsexg  4926  copsex2g  4928  ralxpf  5238  dmcoss  5355  fv3  6173  tz6.12c  6180  opabiota  6228  0neqopab  6663  zfregcl  8459  zfregclOLD  8461  scottex  8708  scott0  8709  dfac5lem5  8910  zfcndpow  9398  zfcndreg  9399  zfcndinf  9400  reclem2pr  9830  mreiincl  16196  brabgaf  29304  cnvoprab  29382  bnj607  30747  bnj900  30760  exisym1  32118  exlimii  32514  bj-exlimmpi  32605  bj-exlimmpbi  32606  bj-exlimmpbir  32607  dihglblem5  36106  eu2ndop1stv  40536