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

Theorem rexlimd 3024
Description: Deduction form of rexlimd 3024. (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 3023 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1705  wcel 1992  wrex 2913
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 1841  ax-6 1890  ax-7 1937  ax-12 2049
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-ral 2917  df-rex 2918
This theorem is referenced by:  r19.29af2  3073  reusv2lem2  4834  reusv2lem2OLD  4835  ralxfrALT  4852  fvmptt  6257  ffnfv  6344  peano5  7037  tz7.49  7486  nneneq  8088  ac6sfi  8149  ixpiunwdom  8441  r1val1  8594  rankuni2b  8661  infpssrlem4  9073  zorn2lem4  9266  zorn2lem5  9267  konigthlem  9335  tskuni  9550  gruiin  9577  lbzbi  11720  fprodle  14647  iunconnlem  21135  ptbasfi  21289  alexsubALTlem3  21758  ovoliunnul  23177  iunmbl2  23227  mptelee  25670  atom1d  29052  elabreximd  29186  iundisjf  29238  esumc  29886  poimirlem24  33051  poimirlem26  33053  poimirlem27  33054  heicant  33062  indexa  33146  sdclem2  33156  glbconxN  34130  cdleme26ee  35114  cdleme32d  35198  cdleme32f  35200  cdlemk38  35669  cdlemk19x  35697  cdlemk11t  35700  refsumcn  38658  eliuniin2  38777  suprnmpt  38815  dffo3f  38824  wessf1ornlem  38831  disjf1o  38838  disjinfi  38840  funimassd  38892  rnmptlb  38915  rnmptbddlem  38917  fvelimad  38920  rnmptbd2lem  38926  infnsuprnmpt  38928  upbdrech  38970  ssfiunibd  38974  iuneqfzuzlem  39001  infrpge  39018  xrralrecnnle  39053  supxrleubrnmpt  39083  infleinf2  39092  suprleubrnmpt  39100  infrnmptle  39101  infxrunb3rnmpt  39106  iccshift  39142  iooshift  39146  fmul01lt1  39209  islptre  39242  rexlim2d  39248  limcperiod  39251  islpcn  39262  limclner  39274  fnlimfvre  39297  climinf2lem  39329  limsupmnflem  39343  limsupre3uzlem  39358  dvnprodlem1  39454  dvnprodlem2  39455  itgperiod  39491  stoweidlem29  39540  stoweidlem31  39542  stoweidlem59  39570  stirlinglem13  39597  fourierdlem48  39665  fourierdlem51  39668  fourierdlem53  39670  fourierdlem80  39697  fourierdlem81  39698  fourierdlem93  39710  elaa2  39745  salexct  39846  sge00  39887  sge0f1o  39893  sge0gerp  39906  sge0lefi  39909  sge0ltfirp  39911  sge0resplit  39917  sge0iunmptlemre  39926  sge0iunmpt  39929  sge0isum  39938  sge0xp  39940  sge0reuz  39958  sge0reuzb  39959  iundjiun  39971  voliunsge0lem  39983  meaiininc2  39996  isomenndlem  40038  ovncvrrp  40072  ovnsubaddlem1  40078  hoidmvval0  40095  hoidmvlelem1  40103  vonioo  40190  vonicc  40193  smfaddlem1  40265  smfresal  40289  smfpimbor1lem2  40300  smflimmpt  40310  smfinflem  40317  smflimsuplem7  40326  smflimsuplem8  40327  smflimsupmpt  40329  ffnafv  40542  iccpartdisj  40659  2zrngagrp  41204  iunord  41688
  Copyright terms: Public domain W3C validator