Theorem rexlimd 3244

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2114  ∃wrex 3061

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 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3052  df-rex 3062

This theorem is referenced by:  r19.29af2  3245  iuneqconst  4945  reusv2lem2  5341  ralxfrALT  5357  funimassd  6906  fvelimad  6907  fvmptt  6968  dffo3f  7058  ffnfv  7071  frpoins3xpg  8090  frpoins3xp3g  8091  tz7.49  8384  nneneq  9140  ac6sfi  9194  ixpiunwdom  9505  r1val1  9710  rankuni2b  9777  infpssrlem4  10228  zorn2lem4  10421  zorn2lem5  10422  konigthlem  10491  tskuni  10706  gruiin  10733  lbzbi  12886  reuccatpfxs1  14709  iunconnlem  23392  ptbasfi  23546  alexsubALTlem3  24014  ovoliunnul  25474  iunmbl2  25524  mpteleeOLD  28964  atom1d  32424  elabreximd  32580  iundisjf  32659  esumc  34195  fvineqsneu  37727  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  heicant  37976  indexa  38054  sdclem2  38063  glbconxN  39824  cdleme26ee  40806  cdleme32d  40890  cdleme32f  40892  cdlemk38  41361  cdlemk19x  41389  cdlemk11t  41392  unielss  43646  oaun3lem1  43802  refsumcn  45461  eliuniin2  45550  rexlimd3  45574  suprnmpt  45604  disjf1o  45621  disjinfi  45622  rnmptlb  45672  rnmptbddlem  45673  rnmptbd2lem  45677  infnsuprnmpt  45679  upbdrech  45738  ssfiunibd  45742  iuneqfzuzlem  45764  infrpge  45781  xrralrecnnle  45812  supxrleubrnmpt  45834  infleinf2  45842  suprleubrnmpt  45850  infrnmptle  45851  infxrunb3rnmpt  45856  infxrgelbrnmpt  45882  iccshift  45948  iooshift  45952  fmul01lt1  46016  islptre  46049  rexlim2d  46055  limcperiod  46058  islpcn  46067  limclner  46079  fnlimfvre  46102  climinf2lem  46134  limsupmnflem  46148  limsupre3uzlem  46163  climuzlem  46171  dvnprodlem1  46374  dvnprodlem2  46375  itgperiod  46409  stoweidlem29  46457  stoweidlem31  46459  stoweidlem59  46487  stirlinglem13  46514  fourierdlem48  46582  fourierdlem51  46585  fourierdlem80  46614  fourierdlem81  46615  fourierdlem93  46627  elaa2  46662  salexct  46762  sge00  46804  sge0f1o  46810  sge0gerp  46823  sge0lefi  46826  sge0ltfirp  46828  sge0resplit  46834  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0isum  46855  sge0xp  46857  sge0reuz  46875  sge0reuzb  46876  iundjiun  46888  voliunsge0lem  46900  meaiuninc3v  46912  meaiininc2  46916  isomenndlem  46958  ovncvrrp  46992  ovnsubaddlem1  46998  hoidmvval0  47015  hoidmvlelem1  47023  vonioo  47110  vonicc  47113  smfaddlem1  47191  smfresal  47216  smfpimbor1lem2  47227  smflimmpt  47238  smfinflem  47245  smflimsuplem7  47254  smflimsuplem8  47255  smflimsupmpt  47257  smfliminfmpt  47260  ffnafv  47619  f1oresf1o2  47739  iccpartdisj  47897  mogoldbb  48261  2zrngagrp  48725  iunord  50151