Theorem rexlimd 3240

Description: Deduction form of rexlimd 3240. For a version based on fewer axioms see rexlimdv 3132. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)

Hypotheses

Ref	Expression
rexlimd.1	⊢ Ⅎ𝑥𝜑
rexlimd.2	⊢ Ⅎ𝑥𝜒
rexlimd.3	⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimd	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Proof of Theorem rexlimd

Step	Hyp	Ref	Expression
1		rexlimd.1	. 2 ⊢ Ⅎ𝑥𝜑
2		rexlimd.2	. . 3 ⊢ Ⅎ𝑥𝜒
3	2	a1i 11	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜒)
4		rexlimd.3	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
5	1, 3, 4	rexlimd2 3239	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3049  df-rex 3058

This theorem is referenced by:  r19.29af2  3241  iuneqconst  4953  reusv2lem2  5339  ralxfrALT  5355  funimassd  6894  fvelimad  6895  fvmptt  6955  dffo3f  7045  ffnfv  7058  frpoins3xpg  8076  frpoins3xp3g  8077  tz7.49  8370  nneneq  9122  ac6sfi  9175  ixpiunwdom  9483  r1val1  9686  rankuni2b  9753  infpssrlem4  10204  zorn2lem4  10397  zorn2lem5  10398  konigthlem  10466  tskuni  10681  gruiin  10708  lbzbi  12836  reuccatpfxs1  14656  iunconnlem  23343  ptbasfi  23497  alexsubALTlem3  23965  ovoliunnul  25436  iunmbl2  25486  mpteleeOLD  28875  atom1d  32335  elabreximd  32492  iundisjf  32571  esumc  34085  fvineqsneu  37476  poimirlem24  37704  poimirlem26  37706  poimirlem27  37707  heicant  37715  indexa  37793  sdclem2  37802  glbconxN  39497  cdleme26ee  40479  cdleme32d  40563  cdleme32f  40565  cdlemk38  41034  cdlemk19x  41062  cdlemk11t  41065  unielss  43335  oaun3lem1  43491  refsumcn  45151  eliuniin2  45241  rexlimd3  45265  suprnmpt  45295  disjf1o  45312  disjinfi  45313  rnmptlb  45364  rnmptbddlem  45365  rnmptbd2lem  45369  infnsuprnmpt  45371  upbdrech  45430  ssfiunibd  45434  iuneqfzuzlem  45457  infrpge  45474  xrralrecnnle  45505  supxrleubrnmpt  45528  infleinf2  45536  suprleubrnmpt  45544  infrnmptle  45545  infxrunb3rnmpt  45550  infxrgelbrnmpt  45576  iccshift  45642  iooshift  45646  fmul01lt1  45710  islptre  45743  rexlim2d  45749  limcperiod  45752  islpcn  45761  limclner  45773  fnlimfvre  45796  climinf2lem  45828  limsupmnflem  45842  limsupre3uzlem  45857  climuzlem  45865  dvnprodlem1  46068  dvnprodlem2  46069  itgperiod  46103  stoweidlem29  46151  stoweidlem31  46153  stoweidlem59  46181  stirlinglem13  46208  fourierdlem48  46276  fourierdlem51  46279  fourierdlem80  46308  fourierdlem81  46309  fourierdlem93  46321  elaa2  46356  salexct  46456  sge00  46498  sge0f1o  46504  sge0gerp  46517  sge0lefi  46520  sge0ltfirp  46522  sge0resplit  46528  sge0iunmptlemre  46537  sge0iunmpt  46540  sge0isum  46549  sge0xp  46551  sge0reuz  46569  sge0reuzb  46570  iundjiun  46582  voliunsge0lem  46594  meaiuninc3v  46606  meaiininc2  46610  isomenndlem  46652  ovncvrrp  46686  ovnsubaddlem1  46692  hoidmvval0  46709  hoidmvlelem1  46717  vonioo  46804  vonicc  46807  smfaddlem1  46885  smfresal  46910  smfpimbor1lem2  46921  smflimmpt  46932  smfinflem  46939  smflimsuplem7  46948  smflimsuplem8  46949  smflimsupmpt  46951  smfliminfmpt  46954  ffnafv  47295  f1oresf1o2  47415  iccpartdisj  47561  mogoldbb  47909  2zrngagrp  48373  iunord  49801