Theorem rexlimd 3276

Description: Deduction form of rexlimd 3276. (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 3275	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2111  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3111  df-rex 3112

This theorem is referenced by:  r19.29af2  3288  iuneqconst  4892  reusv2lem2  5265  ralxfrALT  5281  fvelimad  6707  fvmptt  6765  ffnfv  6859  peano5  7585  tz7.49  8064  nneneq  8684  ac6sfi  8746  ixpiunwdom  9038  r1val1  9199  rankuni2b  9266  infpssrlem4  9717  zorn2lem4  9910  zorn2lem5  9911  konigthlem  9979  tskuni  10194  gruiin  10221  lbzbi  12324  reuccatpfxs1  14100  iunconnlem  22032  ptbasfi  22186  alexsubALTlem3  22654  ovoliunnul  24111  iunmbl2  24161  mptelee  26689  atom1d  30136  elabreximd  30278  iundisjf  30352  esumc  31420  fvineqsneu  34828  poimirlem24  35081  poimirlem26  35083  poimirlem27  35084  heicant  35092  indexa  35171  sdclem2  35180  glbconxN  36674  cdleme26ee  37656  cdleme32d  37740  cdleme32f  37742  cdlemk38  38211  cdlemk19x  38239  cdlemk11t  38242  refsumcn  41659  eliuniin2  41755  rexlimd3  41781  suprnmpt  41798  disjf1o  41818  disjinfi  41820  funimassd  41863  rnmptlb  41880  rnmptbddlem  41881  rnmptbd2lem  41886  infnsuprnmpt  41888  upbdrech  41937  ssfiunibd  41941  iuneqfzuzlem  41966  infrpge  41983  xrralrecnnle  42017  supxrleubrnmpt  42043  infleinf2  42051  suprleubrnmpt  42059  infrnmptle  42060  infxrunb3rnmpt  42065  infxrgelbrnmpt  42093  iccshift  42155  iooshift  42159  fmul01lt1  42228  islptre  42261  rexlim2d  42267  limcperiod  42270  islpcn  42281  limclner  42293  fnlimfvre  42316  climinf2lem  42348  limsupmnflem  42362  limsupre3uzlem  42377  climuzlem  42385  dvnprodlem1  42588  dvnprodlem2  42589  itgperiod  42623  stoweidlem29  42671  stoweidlem31  42673  stoweidlem59  42701  stirlinglem13  42728  fourierdlem48  42796  fourierdlem51  42799  fourierdlem53  42801  fourierdlem80  42828  fourierdlem81  42829  fourierdlem93  42841  elaa2  42876  salexct  42974  sge00  43015  sge0f1o  43021  sge0gerp  43034  sge0lefi  43037  sge0ltfirp  43039  sge0resplit  43045  sge0iunmptlemre  43054  sge0iunmpt  43057  sge0isum  43066  sge0xp  43068  sge0reuz  43086  sge0reuzb  43087  iundjiun  43099  voliunsge0lem  43111  meaiuninc3v  43123  meaiininc2  43127  isomenndlem  43169  ovncvrrp  43203  ovnsubaddlem1  43209  hoidmvval0  43226  hoidmvlelem1  43234  vonioo  43321  vonicc  43324  smfaddlem1  43396  smfresal  43420  smfpimbor1lem2  43431  smflimmpt  43441  smfinflem  43448  smflimsuplem7  43457  smflimsuplem8  43458  smflimsupmpt  43460  smfliminfmpt  43463  ffnafv  43727  f1oresf1o2  43847  iccpartdisj  43954  mogoldbb  44303  2zrngagrp  44567  iunord  45206