Theorem rexlimd 3245

Description: Deduction form of rexlimd 3245. For a version based on fewer axioms see rexlimdv 3133. (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 1783   ∈ wcel 2109  ∃wrex 3054

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 3046  df-rex 3055

This theorem is referenced by:  r19.29af2  3246  iuneqconst  4970  reusv2lem2  5357  ralxfrALT  5373  funimassd  6930  fvelimad  6931  fvmptt  6991  dffo3f  7081  ffnfv  7094  frpoins3xpg  8122  frpoins3xp3g  8123  tz7.49  8416  nneneq  9176  ac6sfi  9238  ixpiunwdom  9550  r1val1  9746  rankuni2b  9813  infpssrlem4  10266  zorn2lem4  10459  zorn2lem5  10460  konigthlem  10528  tskuni  10743  gruiin  10770  lbzbi  12902  reuccatpfxs1  14719  iunconnlem  23321  ptbasfi  23475  alexsubALTlem3  23943  ovoliunnul  25415  iunmbl2  25465  mptelee  28829  atom1d  32289  elabreximd  32446  iundisjf  32525  esumc  34048  fvineqsneu  37406  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  heicant  37656  indexa  37734  sdclem2  37743  glbconxN  39379  cdleme26ee  40361  cdleme32d  40445  cdleme32f  40447  cdlemk38  40916  cdlemk19x  40944  cdlemk11t  40947  unielss  43214  oaun3lem1  43370  refsumcn  45031  eliuniin2  45121  rexlimd3  45145  suprnmpt  45175  disjf1o  45192  disjinfi  45193  rnmptlb  45244  rnmptbddlem  45245  rnmptbd2lem  45249  infnsuprnmpt  45251  upbdrech  45310  ssfiunibd  45314  iuneqfzuzlem  45337  infrpge  45354  xrralrecnnle  45386  supxrleubrnmpt  45409  infleinf2  45417  suprleubrnmpt  45425  infrnmptle  45426  infxrunb3rnmpt  45431  infxrgelbrnmpt  45457  iccshift  45523  iooshift  45527  fmul01lt1  45591  islptre  45624  rexlim2d  45630  limcperiod  45633  islpcn  45644  limclner  45656  fnlimfvre  45679  climinf2lem  45711  limsupmnflem  45725  limsupre3uzlem  45740  climuzlem  45748  dvnprodlem1  45951  dvnprodlem2  45952  itgperiod  45986  stoweidlem29  46034  stoweidlem31  46036  stoweidlem59  46064  stirlinglem13  46091  fourierdlem48  46159  fourierdlem51  46162  fourierdlem80  46191  fourierdlem81  46192  fourierdlem93  46204  elaa2  46239  salexct  46339  sge00  46381  sge0f1o  46387  sge0gerp  46400  sge0lefi  46403  sge0ltfirp  46405  sge0resplit  46411  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0isum  46432  sge0xp  46434  sge0reuz  46452  sge0reuzb  46453  iundjiun  46465  voliunsge0lem  46477  meaiuninc3v  46489  meaiininc2  46493  isomenndlem  46535  ovncvrrp  46569  ovnsubaddlem1  46575  hoidmvval0  46592  hoidmvlelem1  46600  vonioo  46687  vonicc  46690  smfaddlem1  46768  smfresal  46793  smfpimbor1lem2  46804  smflimmpt  46815  smfinflem  46822  smflimsuplem7  46831  smflimsuplem8  46832  smflimsupmpt  46834  smfliminfmpt  46837  ffnafv  47176  f1oresf1o2  47296  iccpartdisj  47442  mogoldbb  47790  2zrngagrp  48241  iunord  49669