MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 rexlimd.1 . 2 𝑥𝜑
2 rexlimd.2 . . 3 𝑥𝜒
32a1i 11 . 2 (𝜑 → Ⅎ𝑥𝜒)
4 rexlimd.3 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
51, 3, 4rexlimd2 3316 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
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 2173
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  4929  reusv2lem2  5299  ralxfrALT  5315  fvelimad  6731  fvmptt  6787  ffnfv  6881  peano5  7604  tz7.49  8080  nneneq  8699  ac6sfi  8761  ixpiunwdom  9054  r1val1  9214  rankuni2b  9281  infpssrlem4  9727  zorn2lem4  9920  zorn2lem5  9921  konigthlem  9989  tskuni  10204  gruiin  10231  lbzbi  12335  reuccatpfxs1  14108  iunconnlem  22034  ptbasfi  22188  alexsubALTlem3  22656  ovoliunnul  24107  iunmbl2  24157  mptelee  26680  atom1d  30129  elabreximd  30269  iundisjf  30338  esumc  31310  fvineqsneu  34691  poimirlem24  34915  poimirlem26  34917  poimirlem27  34918  heicant  34926  indexa  35007  sdclem2  35016  glbconxN  36513  cdleme26ee  37495  cdleme32d  37579  cdleme32f  37581  cdlemk38  38050  cdlemk19x  38078  cdlemk11t  38081  refsumcn  41285  eliuniin2  41384  rexlimd3  41411  suprnmpt  41428  disjf1o  41450  disjinfi  41452  funimassd  41495  rnmptlb  41512  rnmptbddlem  41513  rnmptbd2lem  41518  infnsuprnmpt  41520  upbdrech  41570  ssfiunibd  41574  iuneqfzuzlem  41600  infrpge  41617  xrralrecnnle  41651  supxrleubrnmpt  41677  infleinf2  41686  suprleubrnmpt  41694  infrnmptle  41695  infxrunb3rnmpt  41700  infxrgelbrnmpt  41728  iccshift  41792  iooshift  41796  fmul01lt1  41865  islptre  41898  rexlim2d  41904  limcperiod  41907  islpcn  41918  limclner  41930  fnlimfvre  41953  climinf2lem  41985  limsupmnflem  41999  limsupre3uzlem  42014  climuzlem  42022  dvnprodlem1  42229  dvnprodlem2  42230  itgperiod  42264  stoweidlem29  42313  stoweidlem31  42315  stoweidlem59  42343  stirlinglem13  42370  fourierdlem48  42438  fourierdlem51  42441  fourierdlem53  42443  fourierdlem80  42470  fourierdlem81  42471  fourierdlem93  42483  elaa2  42518  salexct  42616  sge00  42657  sge0f1o  42663  sge0gerp  42676  sge0lefi  42679  sge0ltfirp  42681  sge0resplit  42687  sge0iunmptlemre  42696  sge0iunmpt  42699  sge0isum  42708  sge0xp  42710  sge0reuz  42728  sge0reuzb  42729  iundjiun  42741  voliunsge0lem  42753  meaiuninc3v  42765  meaiininc2  42769  isomenndlem  42811  ovncvrrp  42845  ovnsubaddlem1  42851  hoidmvval0  42868  hoidmvlelem1  42876  vonioo  42963  vonicc  42966  smfaddlem1  43038  smfresal  43062  smfpimbor1lem2  43073  smflimmpt  43083  smfinflem  43090  smflimsuplem7  43099  smflimsuplem8  43100  smflimsupmpt  43102  smfliminfmpt  43105  ffnafv  43369  f1oresf1o2  43489  iccpartdisj  43596  mogoldbb  43949  2zrngagrp  44213  iunord  44778
  Copyright terms: Public domain W3C validator