Theorem rexlimd 3272

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

Syntax hints:   → wi 4  Ⅎwnf 1781   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-ral 3068  df-rex 3077

This theorem is referenced by:  r19.29af2  3273  iuneqconst  5026  reusv2lem2  5417  ralxfrALT  5433  funimassd  6988  fvelimad  6989  fvmptt  7049  dffo3f  7140  ffnfv  7153  peano5OLD  7933  frpoins3xpg  8181  frpoins3xp3g  8182  tz7.49  8501  nneneq  9272  nneneqOLD  9284  ac6sfi  9348  ixpiunwdom  9659  r1val1  9855  rankuni2b  9922  infpssrlem4  10375  zorn2lem4  10568  zorn2lem5  10569  konigthlem  10637  tskuni  10852  gruiin  10879  lbzbi  13001  reuccatpfxs1  14795  iunconnlem  23456  ptbasfi  23610  alexsubALTlem3  24078  ovoliunnul  25561  iunmbl2  25611  mptelee  28928  atom1d  32385  elabreximd  32538  iundisjf  32611  esumc  34015  fvineqsneu  37377  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  heicant  37615  indexa  37693  sdclem2  37702  glbconxN  39335  cdleme26ee  40317  cdleme32d  40401  cdleme32f  40403  cdlemk38  40872  cdlemk19x  40900  cdlemk11t  40903  unielss  43179  oaun3lem1  43336  refsumcn  44930  eliuniin2  45022  rexlimd3  45046  suprnmpt  45081  disjf1o  45098  disjinfi  45099  rnmptlb  45152  rnmptbddlem  45153  rnmptbd2lem  45157  infnsuprnmpt  45159  upbdrech  45220  ssfiunibd  45224  iuneqfzuzlem  45249  infrpge  45266  xrralrecnnle  45298  supxrleubrnmpt  45321  infleinf2  45329  suprleubrnmpt  45337  infrnmptle  45338  infxrunb3rnmpt  45343  infxrgelbrnmpt  45369  iccshift  45436  iooshift  45440  fmul01lt1  45507  islptre  45540  rexlim2d  45546  limcperiod  45549  islpcn  45560  limclner  45572  fnlimfvre  45595  climinf2lem  45627  limsupmnflem  45641  limsupre3uzlem  45656  climuzlem  45664  dvnprodlem1  45867  dvnprodlem2  45868  itgperiod  45902  stoweidlem29  45950  stoweidlem31  45952  stoweidlem59  45980  stirlinglem13  46007  fourierdlem48  46075  fourierdlem51  46078  fourierdlem80  46107  fourierdlem81  46108  fourierdlem93  46120  elaa2  46155  salexct  46255  sge00  46297  sge0f1o  46303  sge0gerp  46316  sge0lefi  46319  sge0ltfirp  46321  sge0resplit  46327  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0isum  46348  sge0xp  46350  sge0reuz  46368  sge0reuzb  46369  iundjiun  46381  voliunsge0lem  46393  meaiuninc3v  46405  meaiininc2  46409  isomenndlem  46451  ovncvrrp  46485  ovnsubaddlem1  46491  hoidmvval0  46508  hoidmvlelem1  46516  vonioo  46603  vonicc  46606  smfaddlem1  46684  smfresal  46709  smfpimbor1lem2  46720  smflimmpt  46731  smfinflem  46738  smflimsuplem7  46747  smflimsuplem8  46748  smflimsupmpt  46750  smfliminfmpt  46753  ffnafv  47086  f1oresf1o2  47206  iccpartdisj  47311  mogoldbb  47659  2zrngagrp  47972  iunord  48768