Theorem rexlimd 3253

Description: Deduction form of rexlimd 3253. For a version based on fewer axioms see rexlimdv 3140. (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 3252	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3053  df-rex 3062

This theorem is referenced by:  r19.29af2  3254  iuneqconst  4984  reusv2lem2  5374  ralxfrALT  5390  funimassd  6950  fvelimad  6951  fvmptt  7011  dffo3f  7101  ffnfv  7114  frpoins3xpg  8144  frpoins3xp3g  8145  tz7.49  8464  nneneq  9225  ac6sfi  9297  ixpiunwdom  9609  r1val1  9805  rankuni2b  9872  infpssrlem4  10325  zorn2lem4  10518  zorn2lem5  10519  konigthlem  10587  tskuni  10802  gruiin  10829  lbzbi  12957  reuccatpfxs1  14770  iunconnlem  23370  ptbasfi  23524  alexsubALTlem3  23992  ovoliunnul  25465  iunmbl2  25515  mptelee  28879  atom1d  32339  elabreximd  32496  iundisjf  32575  esumc  34087  fvineqsneu  37434  poimirlem24  37673  poimirlem26  37675  poimirlem27  37676  heicant  37684  indexa  37762  sdclem2  37771  glbconxN  39402  cdleme26ee  40384  cdleme32d  40468  cdleme32f  40470  cdlemk38  40939  cdlemk19x  40967  cdlemk11t  40970  unielss  43209  oaun3lem1  43365  refsumcn  45021  eliuniin2  45111  rexlimd3  45135  suprnmpt  45165  disjf1o  45182  disjinfi  45183  rnmptlb  45234  rnmptbddlem  45235  rnmptbd2lem  45239  infnsuprnmpt  45241  upbdrech  45301  ssfiunibd  45305  iuneqfzuzlem  45328  infrpge  45345  xrralrecnnle  45377  supxrleubrnmpt  45400  infleinf2  45408  suprleubrnmpt  45416  infrnmptle  45417  infxrunb3rnmpt  45422  infxrgelbrnmpt  45448  iccshift  45514  iooshift  45518  fmul01lt1  45582  islptre  45615  rexlim2d  45621  limcperiod  45624  islpcn  45635  limclner  45647  fnlimfvre  45670  climinf2lem  45702  limsupmnflem  45716  limsupre3uzlem  45731  climuzlem  45739  dvnprodlem1  45942  dvnprodlem2  45943  itgperiod  45977  stoweidlem29  46025  stoweidlem31  46027  stoweidlem59  46055  stirlinglem13  46082  fourierdlem48  46150  fourierdlem51  46153  fourierdlem80  46182  fourierdlem81  46183  fourierdlem93  46195  elaa2  46230  salexct  46330  sge00  46372  sge0f1o  46378  sge0gerp  46391  sge0lefi  46394  sge0ltfirp  46396  sge0resplit  46402  sge0iunmptlemre  46411  sge0iunmpt  46414  sge0isum  46423  sge0xp  46425  sge0reuz  46443  sge0reuzb  46444  iundjiun  46456  voliunsge0lem  46468  meaiuninc3v  46480  meaiininc2  46484  isomenndlem  46526  ovncvrrp  46560  ovnsubaddlem1  46566  hoidmvval0  46583  hoidmvlelem1  46591  vonioo  46678  vonicc  46681  smfaddlem1  46759  smfresal  46784  smfpimbor1lem2  46795  smflimmpt  46806  smfinflem  46813  smflimsuplem7  46822  smflimsuplem8  46823  smflimsupmpt  46825  smfliminfmpt  46828  ffnafv  47167  f1oresf1o2  47287  iccpartdisj  47418  mogoldbb  47766  2zrngagrp  48191  iunord  49507