Theorem rexlimd 3317

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

Syntax hints:   → wi 4  Ⅎwnf 1780   ∈ wcel 2110  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2172

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  r19.29af2  3330  iuneqconst  4923  reusv2lem2  5292  ralxfrALT  5308  fvelimad  6727  fvmptt  6783  ffnfv  6877  peano5  7599  tz7.49  8075  nneneq  8694  ac6sfi  8756  ixpiunwdom  9049  r1val1  9209  rankuni2b  9276  infpssrlem4  9722  zorn2lem4  9915  zorn2lem5  9916  konigthlem  9984  tskuni  10199  gruiin  10226  lbzbi  12330  reuccatpfxs1  14103  iunconnlem  22029  ptbasfi  22183  alexsubALTlem3  22651  ovoliunnul  24102  iunmbl2  24152  mptelee  26675  atom1d  30124  elabreximd  30264  iundisjf  30333  esumc  31305  fvineqsneu  34686  poimirlem24  34910  poimirlem26  34912  poimirlem27  34913  heicant  34921  indexa  35002  sdclem2  35011  glbconxN  36508  cdleme26ee  37490  cdleme32d  37574  cdleme32f  37576  cdlemk38  38045  cdlemk19x  38073  cdlemk11t  38076  refsumcn  41280  eliuniin2  41379  rexlimd3  41405  suprnmpt  41422  disjf1o  41444  disjinfi  41446  funimassd  41489  rnmptlb  41506  rnmptbddlem  41507  rnmptbd2lem  41512  infnsuprnmpt  41514  upbdrech  41564  ssfiunibd  41568  iuneqfzuzlem  41594  infrpge  41611  xrralrecnnle  41645  supxrleubrnmpt  41671  infleinf2  41680  suprleubrnmpt  41688  infrnmptle  41689  infxrunb3rnmpt  41694  infxrgelbrnmpt  41722  iccshift  41786  iooshift  41790  fmul01lt1  41859  islptre  41892  rexlim2d  41898  limcperiod  41901  islpcn  41912  limclner  41924  fnlimfvre  41947  climinf2lem  41979  limsupmnflem  41993  limsupre3uzlem  42008  climuzlem  42016  dvnprodlem1  42223  dvnprodlem2  42224  itgperiod  42258  stoweidlem29  42307  stoweidlem31  42309  stoweidlem59  42337  stirlinglem13  42364  fourierdlem48  42432  fourierdlem51  42435  fourierdlem53  42437  fourierdlem80  42464  fourierdlem81  42465  fourierdlem93  42477  elaa2  42512  salexct  42610  sge00  42651  sge0f1o  42657  sge0gerp  42670  sge0lefi  42673  sge0ltfirp  42675  sge0resplit  42681  sge0iunmptlemre  42690  sge0iunmpt  42693  sge0isum  42702  sge0xp  42704  sge0reuz  42722  sge0reuzb  42723  iundjiun  42735  voliunsge0lem  42747  meaiuninc3v  42759  meaiininc2  42763  isomenndlem  42805  ovncvrrp  42839  ovnsubaddlem1  42845  hoidmvval0  42862  hoidmvlelem1  42870  vonioo  42957  vonicc  42960  smfaddlem1  43032  smfresal  43056  smfpimbor1lem2  43067  smflimmpt  43077  smfinflem  43084  smflimsuplem7  43093  smflimsuplem8  43094  smflimsupmpt  43096  smfliminfmpt  43099  ffnafv  43363  f1oresf1o2  43483  iccpartdisj  43590  mogoldbb  43943  2zrngagrp  44207  iunord  44772