Theorem rexlimd 3236

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

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

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 3045  df-rex 3054

This theorem is referenced by:  r19.29af2  3237  iuneqconst  4956  reusv2lem2  5341  ralxfrALT  5357  funimassd  6893  fvelimad  6894  fvmptt  6954  dffo3f  7044  ffnfv  7057  frpoins3xpg  8080  frpoins3xp3g  8081  tz7.49  8374  nneneq  9130  ac6sfi  9189  ixpiunwdom  9501  r1val1  9701  rankuni2b  9768  infpssrlem4  10219  zorn2lem4  10412  zorn2lem5  10413  konigthlem  10481  tskuni  10696  gruiin  10723  lbzbi  12855  reuccatpfxs1  14671  iunconnlem  23330  ptbasfi  23484  alexsubALTlem3  23952  ovoliunnul  25424  iunmbl2  25474  mptelee  28858  atom1d  32315  elabreximd  32472  iundisjf  32551  esumc  34017  fvineqsneu  37384  poimirlem24  37623  poimirlem26  37625  poimirlem27  37626  heicant  37634  indexa  37712  sdclem2  37721  glbconxN  39357  cdleme26ee  40339  cdleme32d  40423  cdleme32f  40425  cdlemk38  40894  cdlemk19x  40922  cdlemk11t  40925  unielss  43191  oaun3lem1  43347  refsumcn  45008  eliuniin2  45098  rexlimd3  45122  suprnmpt  45152  disjf1o  45169  disjinfi  45170  rnmptlb  45221  rnmptbddlem  45222  rnmptbd2lem  45226  infnsuprnmpt  45228  upbdrech  45287  ssfiunibd  45291  iuneqfzuzlem  45314  infrpge  45331  xrralrecnnle  45363  supxrleubrnmpt  45386  infleinf2  45394  suprleubrnmpt  45402  infrnmptle  45403  infxrunb3rnmpt  45408  infxrgelbrnmpt  45434  iccshift  45500  iooshift  45504  fmul01lt1  45568  islptre  45601  rexlim2d  45607  limcperiod  45610  islpcn  45621  limclner  45633  fnlimfvre  45656  climinf2lem  45688  limsupmnflem  45702  limsupre3uzlem  45717  climuzlem  45725  dvnprodlem1  45928  dvnprodlem2  45929  itgperiod  45963  stoweidlem29  46011  stoweidlem31  46013  stoweidlem59  46041  stirlinglem13  46068  fourierdlem48  46136  fourierdlem51  46139  fourierdlem80  46168  fourierdlem81  46169  fourierdlem93  46181  elaa2  46216  salexct  46316  sge00  46358  sge0f1o  46364  sge0gerp  46377  sge0lefi  46380  sge0ltfirp  46382  sge0resplit  46388  sge0iunmptlemre  46397  sge0iunmpt  46400  sge0isum  46409  sge0xp  46411  sge0reuz  46429  sge0reuzb  46430  iundjiun  46442  voliunsge0lem  46454  meaiuninc3v  46466  meaiininc2  46470  isomenndlem  46512  ovncvrrp  46546  ovnsubaddlem1  46552  hoidmvval0  46569  hoidmvlelem1  46577  vonioo  46664  vonicc  46667  smfaddlem1  46745  smfresal  46770  smfpimbor1lem2  46781  smflimmpt  46792  smfinflem  46799  smflimsuplem7  46808  smflimsuplem8  46809  smflimsupmpt  46811  smfliminfmpt  46814  ffnafv  47156  f1oresf1o2  47276  iccpartdisj  47422  mogoldbb  47770  2zrngagrp  48234  iunord  49662