Theorem rexlimd 3245

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

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

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 3053  df-rex 3063

This theorem is referenced by:  r19.29af2  3246  iuneqconst  4960  reusv2lem2  5346  ralxfrALT  5362  funimassd  6908  fvelimad  6909  fvmptt  6970  dffo3f  7060  ffnfv  7073  frpoins3xpg  8092  frpoins3xp3g  8093  tz7.49  8386  nneneq  9142  ac6sfi  9196  ixpiunwdom  9507  r1val1  9710  rankuni2b  9777  infpssrlem4  10228  zorn2lem4  10421  zorn2lem5  10422  konigthlem  10491  tskuni  10706  gruiin  10733  lbzbi  12861  reuccatpfxs1  14682  iunconnlem  23383  ptbasfi  23537  alexsubALTlem3  24005  ovoliunnul  25476  iunmbl2  25526  mpteleeOLD  28980  atom1d  32440  elabreximd  32596  iundisjf  32675  esumc  34228  fvineqsneu  37660  poimirlem24  37889  poimirlem26  37891  poimirlem27  37892  heicant  37900  indexa  37978  sdclem2  37987  glbconxN  39748  cdleme26ee  40730  cdleme32d  40814  cdleme32f  40816  cdlemk38  41285  cdlemk19x  41313  cdlemk11t  41316  unielss  43569  oaun3lem1  43725  refsumcn  45384  eliuniin2  45473  rexlimd3  45497  suprnmpt  45527  disjf1o  45544  disjinfi  45545  rnmptlb  45595  rnmptbddlem  45596  rnmptbd2lem  45600  infnsuprnmpt  45602  upbdrech  45661  ssfiunibd  45665  iuneqfzuzlem  45687  infrpge  45704  xrralrecnnle  45735  supxrleubrnmpt  45758  infleinf2  45766  suprleubrnmpt  45774  infrnmptle  45775  infxrunb3rnmpt  45780  infxrgelbrnmpt  45806  iccshift  45872  iooshift  45876  fmul01lt1  45940  islptre  45973  rexlim2d  45979  limcperiod  45982  islpcn  45991  limclner  46003  fnlimfvre  46026  climinf2lem  46058  limsupmnflem  46072  limsupre3uzlem  46087  climuzlem  46095  dvnprodlem1  46298  dvnprodlem2  46299  itgperiod  46333  stoweidlem29  46381  stoweidlem31  46383  stoweidlem59  46411  stirlinglem13  46438  fourierdlem48  46506  fourierdlem51  46509  fourierdlem80  46538  fourierdlem81  46539  fourierdlem93  46551  elaa2  46586  salexct  46686  sge00  46728  sge0f1o  46734  sge0gerp  46747  sge0lefi  46750  sge0ltfirp  46752  sge0resplit  46758  sge0iunmptlemre  46767  sge0iunmpt  46770  sge0isum  46779  sge0xp  46781  sge0reuz  46799  sge0reuzb  46800  iundjiun  46812  voliunsge0lem  46824  meaiuninc3v  46836  meaiininc2  46840  isomenndlem  46882  ovncvrrp  46916  ovnsubaddlem1  46922  hoidmvval0  46939  hoidmvlelem1  46947  vonioo  47034  vonicc  47037  smfaddlem1  47115  smfresal  47140  smfpimbor1lem2  47151  smflimmpt  47162  smfinflem  47169  smflimsuplem7  47178  smflimsuplem8  47179  smflimsupmpt  47181  smfliminfmpt  47184  ffnafv  47525  f1oresf1o2  47645  iccpartdisj  47791  mogoldbb  48139  2zrngagrp  48603  iunord  50029