Theorem rexlimd 3228

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

Syntax hints:   → wi 4  Ⅎwnf 1790   ∈ wcel 2114  ∃wrex 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-nf 1791  df-ral 3059  df-rex 3060

This theorem is referenced by:  r19.29af2  3240  iuneqconst  4893  reusv2lem2  5267  ralxfrALT  5283  fvelimad  6739  fvmptt  6798  ffnfv  6895  peano5OLD  7628  tz7.49  8113  nneneq  8753  ac6sfi  8839  ixpiunwdom  9130  r1val1  9291  rankuni2b  9358  infpssrlem4  9809  zorn2lem4  10002  zorn2lem5  10003  konigthlem  10071  tskuni  10286  gruiin  10313  lbzbi  12421  reuccatpfxs1  14201  iunconnlem  22181  ptbasfi  22335  alexsubALTlem3  22803  ovoliunnul  24262  iunmbl2  24312  mptelee  26844  atom1d  30291  elabreximd  30432  iundisjf  30505  esumc  31592  frpoins3xpg  33393  frpoins3xp3g  33394  fvineqsneu  35228  poimirlem24  35447  poimirlem26  35449  poimirlem27  35450  heicant  35458  indexa  35537  sdclem2  35546  glbconxN  37038  cdleme26ee  38020  cdleme32d  38104  cdleme32f  38106  cdlemk38  38575  cdlemk19x  38603  cdlemk11t  38606  refsumcn  42134  eliuniin2  42230  rexlimd3  42254  suprnmpt  42271  disjf1o  42290  disjinfi  42292  funimassd  42331  rnmptlb  42348  rnmptbddlem  42349  rnmptbd2lem  42354  infnsuprnmpt  42356  upbdrech  42405  ssfiunibd  42409  iuneqfzuzlem  42434  infrpge  42451  xrralrecnnle  42483  supxrleubrnmpt  42507  infleinf2  42515  suprleubrnmpt  42523  infrnmptle  42524  infxrunb3rnmpt  42529  infxrgelbrnmpt  42557  iccshift  42619  iooshift  42623  fmul01lt1  42692  islptre  42725  rexlim2d  42731  limcperiod  42734  islpcn  42745  limclner  42757  fnlimfvre  42780  climinf2lem  42812  limsupmnflem  42826  limsupre3uzlem  42841  climuzlem  42849  dvnprodlem1  43052  dvnprodlem2  43053  itgperiod  43087  stoweidlem29  43135  stoweidlem31  43137  stoweidlem59  43165  stirlinglem13  43192  fourierdlem48  43260  fourierdlem51  43263  fourierdlem80  43292  fourierdlem81  43293  fourierdlem93  43305  elaa2  43340  salexct  43438  sge00  43479  sge0f1o  43485  sge0gerp  43498  sge0lefi  43501  sge0ltfirp  43503  sge0resplit  43509  sge0iunmptlemre  43518  sge0iunmpt  43521  sge0isum  43530  sge0xp  43532  sge0reuz  43550  sge0reuzb  43551  iundjiun  43563  voliunsge0lem  43575  meaiuninc3v  43587  meaiininc2  43591  isomenndlem  43633  ovncvrrp  43667  ovnsubaddlem1  43673  hoidmvval0  43690  hoidmvlelem1  43698  vonioo  43785  vonicc  43788  smfaddlem1  43860  smfresal  43884  smfpimbor1lem2  43895  smflimmpt  43905  smfinflem  43912  smflimsuplem7  43921  smflimsuplem8  43922  smflimsupmpt  43924  smfliminfmpt  43927  ffnafv  44226  f1oresf1o2  44346  iccpartdisj  44453  mogoldbb  44801  2zrngagrp  45065  iunord  45865