Theorem exlimi 2086

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

Syntax hints:   → wi 4  ∃wex 1704  Ⅎwnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1705  df-nf 1710

This theorem is referenced by:  exlimih  2148  equs5aALT  2177  equs5eALT  2178  equsex  2292  nfeqf2  2297  exdistrf  2333  equs5a  2348  equs5e  2349  mo2v  2477  moanim  2529  euan  2530  moexex  2541  2eu6  2558  ceqsex  3241  sbhypf  3253  vtoclgf  3264  vtoclg1f  3265  vtoclef  3281  rspn0  3934  reusv2lem1  4868  copsexg  4956  copsex2g  4958  ralxpf  5268  dmcoss  5385  fv3  6206  tz6.12c  6213  opabiota  6261  0neqopab  6698  zfregcl  8499  zfregclOLD  8501  scottex  8748  scott0  8749  dfac5lem5  8950  zfcndpow  9438  zfcndreg  9439  zfcndinf  9440  reclem2pr  9870  mreiincl  16256  brabgaf  29420  cnvoprab  29498  bnj607  30986  bnj900  30999  exisym1  32423  exlimii  32818  bj-exlimmpi  32905  bj-exlimmpbi  32906  bj-exlimmpbir  32907  dihglblem5  36587  eu2ndop1stv  41202