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

Theorem rexlimd 3021
Description: Deduction form of rexlimd 3021. (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 3020 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1705  wcel 1987  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-ral 2913  df-rex 2914
This theorem is referenced by:  r19.29af2  3070  reusv2lem2  4839  reusv2lem2OLD  4840  ralxfrALT  4857  fvmptt  6266  ffnfv  6354  peano5  7051  tz7.49  7500  nneneq  8103  ac6sfi  8164  ixpiunwdom  8456  r1val1  8609  rankuni2b  8676  infpssrlem4  9088  zorn2lem4  9281  zorn2lem5  9282  konigthlem  9350  tskuni  9565  gruiin  9592  lbzbi  11736  fprodle  14671  iunconnlem  21170  ptbasfi  21324  alexsubALTlem3  21793  ovoliunnul  23215  iunmbl2  23265  mptelee  25709  atom1d  29100  elabreximd  29236  iundisjf  29288  esumc  29936  poimirlem24  33104  poimirlem26  33106  poimirlem27  33107  heicant  33115  indexa  33199  sdclem2  33209  glbconxN  34183  cdleme26ee  35167  cdleme32d  35251  cdleme32f  35253  cdlemk38  35722  cdlemk19x  35750  cdlemk11t  35753  refsumcn  38711  eliuniin2  38828  suprnmpt  38864  dffo3f  38873  wessf1ornlem  38880  disjf1o  38887  disjinfi  38889  funimassd  38941  rnmptlb  38963  rnmptbddlem  38965  fvelimad  38968  rnmptbd2lem  38974  infnsuprnmpt  38976  upbdrech  39018  ssfiunibd  39022  iuneqfzuzlem  39049  infrpge  39066  xrralrecnnle  39101  supxrleubrnmpt  39131  infleinf2  39140  suprleubrnmpt  39148  infrnmptle  39149  infxrunb3rnmpt  39154  iccshift  39190  iooshift  39194  fmul01lt1  39254  islptre  39287  rexlim2d  39293  limcperiod  39296  islpcn  39307  limclner  39319  fnlimfvre  39342  climinf2lem  39374  limsupmnflem  39388  limsupre3uzlem  39403  dvnprodlem1  39498  dvnprodlem2  39499  itgperiod  39534  stoweidlem29  39583  stoweidlem31  39585  stoweidlem59  39613  stirlinglem13  39640  fourierdlem48  39708  fourierdlem51  39711  fourierdlem53  39713  fourierdlem80  39740  fourierdlem81  39741  fourierdlem93  39753  elaa2  39788  salexct  39889  sge00  39930  sge0f1o  39936  sge0gerp  39949  sge0lefi  39952  sge0ltfirp  39954  sge0resplit  39960  sge0iunmptlemre  39969  sge0iunmpt  39972  sge0isum  39981  sge0xp  39983  sge0reuz  40001  sge0reuzb  40002  iundjiun  40014  voliunsge0lem  40026  meaiininc2  40039  isomenndlem  40081  ovncvrrp  40115  ovnsubaddlem1  40121  hoidmvval0  40138  hoidmvlelem1  40146  vonioo  40233  vonicc  40236  smfaddlem1  40308  smfresal  40332  smfpimbor1lem2  40343  smflimmpt  40353  smfinflem  40360  smflimsuplem7  40369  smflimsuplem8  40370  smflimsupmpt  40372  ffnafv  40585  iccpartdisj  40701  2zrngagrp  41261  iunord  41744
  Copyright terms: Public domain W3C validator