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  4953  reusv2lem2  5338  ralxfrALT  5354  funimassd  6889  fvelimad  6890  fvmptt  6950  dffo3f  7040  ffnfv  7053  frpoins3xpg  8073  frpoins3xp3g  8074  tz7.49  8367  nneneq  9120  ac6sfi  9173  ixpiunwdom  9482  r1val1  9682  rankuni2b  9749  infpssrlem4  10200  zorn2lem4  10393  zorn2lem5  10394  konigthlem  10462  tskuni  10677  gruiin  10704  lbzbi  12837  reuccatpfxs1  14653  iunconnlem  23312  ptbasfi  23466  alexsubALTlem3  23934  ovoliunnul  25406  iunmbl2  25456  mptelee  28840  atom1d  32297  elabreximd  32454  iundisjf  32533  esumc  34024  fvineqsneu  37395  poimirlem24  37634  poimirlem26  37636  poimirlem27  37637  heicant  37645  indexa  37723  sdclem2  37732  glbconxN  39367  cdleme26ee  40349  cdleme32d  40433  cdleme32f  40435  cdlemk38  40904  cdlemk19x  40932  cdlemk11t  40935  unielss  43201  oaun3lem1  43357  refsumcn  45018  eliuniin2  45108  rexlimd3  45132  suprnmpt  45162  disjf1o  45179  disjinfi  45180  rnmptlb  45231  rnmptbddlem  45232  rnmptbd2lem  45236  infnsuprnmpt  45238  upbdrech  45297  ssfiunibd  45301  iuneqfzuzlem  45324  infrpge  45341  xrralrecnnle  45372  supxrleubrnmpt  45395  infleinf2  45403  suprleubrnmpt  45411  infrnmptle  45412  infxrunb3rnmpt  45417  infxrgelbrnmpt  45443  iccshift  45509  iooshift  45513  fmul01lt1  45577  islptre  45610  rexlim2d  45616  limcperiod  45619  islpcn  45630  limclner  45642  fnlimfvre  45665  climinf2lem  45697  limsupmnflem  45711  limsupre3uzlem  45726  climuzlem  45734  dvnprodlem1  45937  dvnprodlem2  45938  itgperiod  45972  stoweidlem29  46020  stoweidlem31  46022  stoweidlem59  46050  stirlinglem13  46077  fourierdlem48  46145  fourierdlem51  46148  fourierdlem80  46177  fourierdlem81  46178  fourierdlem93  46190  elaa2  46225  salexct  46325  sge00  46367  sge0f1o  46373  sge0gerp  46386  sge0lefi  46389  sge0ltfirp  46391  sge0resplit  46397  sge0iunmptlemre  46406  sge0iunmpt  46409  sge0isum  46418  sge0xp  46420  sge0reuz  46438  sge0reuzb  46439  iundjiun  46451  voliunsge0lem  46463  meaiuninc3v  46475  meaiininc2  46479  isomenndlem  46521  ovncvrrp  46555  ovnsubaddlem1  46561  hoidmvval0  46578  hoidmvlelem1  46586  vonioo  46673  vonicc  46676  smfaddlem1  46754  smfresal  46779  smfpimbor1lem2  46790  smflimmpt  46801  smfinflem  46808  smflimsuplem7  46817  smflimsuplem8  46818  smflimsupmpt  46820  smfliminfmpt  46823  ffnafv  47165  f1oresf1o2  47285  iccpartdisj  47431  mogoldbb  47779  2zrngagrp  48243  iunord  49671