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

Theorem rexlimd 3160
Description: Deduction form of rexlimd 3160. (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 3159 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1853  wcel 2135  wrex 3047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-12 2192
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1850  df-nf 1855  df-ral 3051  df-rex 3052
This theorem is referenced by:  r19.29af2  3209  reusv2lem2  5014  reusv2lem2OLD  5015  ralxfrALT  5032  fvmptt  6458  ffnfv  6547  peano5  7250  tz7.49  7705  nneneq  8304  ac6sfi  8365  ixpiunwdom  8657  r1val1  8818  rankuni2b  8885  infpssrlem4  9316  zorn2lem4  9509  zorn2lem5  9510  konigthlem  9578  tskuni  9793  gruiin  9820  lbzbi  11965  reuccats1  13676  fprodle  14922  iunconnlem  21428  ptbasfi  21582  alexsubALTlem3  22050  ovoliunnul  23471  iunmbl2  23521  mptelee  25970  atom1d  29517  elabreximd  29651  iundisjf  29705  esumc  30418  poimirlem24  33742  poimirlem26  33744  poimirlem27  33745  heicant  33753  indexa  33837  sdclem2  33847  glbconxN  35163  cdleme26ee  36146  cdleme32d  36230  cdleme32f  36232  cdlemk38  36701  cdlemk19x  36729  cdlemk11t  36732  refsumcn  39684  eliuniin2  39798  rexlimd3  39830  suprnmpt  39850  dffo3f  39859  wessf1ornlem  39866  disjf1o  39873  disjinfi  39875  funimassd  39926  rnmptlb  39948  rnmptbddlem  39950  fvelimad  39953  rnmptbd2lem  39958  infnsuprnmpt  39960  upbdrech  40014  ssfiunibd  40018  iuneqfzuzlem  40044  infrpge  40061  xrralrecnnle  40096  supxrleubrnmpt  40126  infleinf2  40135  suprleubrnmpt  40143  infrnmptle  40144  infxrunb3rnmpt  40149  infxrgelbrnmpt  40177  iccshift  40243  iooshift  40247  fmul01lt1  40317  islptre  40350  rexlim2d  40356  limcperiod  40359  islpcn  40370  limclner  40382  fnlimfvre  40405  climinf2lem  40437  limsupmnflem  40451  limsupre3uzlem  40466  climuzlem  40474  dvnprodlem1  40660  dvnprodlem2  40661  itgperiod  40696  stoweidlem29  40745  stoweidlem31  40747  stoweidlem59  40775  stirlinglem13  40802  fourierdlem48  40870  fourierdlem51  40873  fourierdlem53  40875  fourierdlem80  40902  fourierdlem81  40903  fourierdlem93  40915  elaa2  40950  salexct  41051  sge00  41092  sge0f1o  41098  sge0gerp  41111  sge0lefi  41114  sge0ltfirp  41116  sge0resplit  41122  sge0iunmptlemre  41131  sge0iunmpt  41134  sge0isum  41143  sge0xp  41145  sge0reuz  41163  sge0reuzb  41164  iundjiun  41176  voliunsge0lem  41188  meaiuninc3v  41200  meaiininc2  41204  isomenndlem  41246  ovncvrrp  41280  ovnsubaddlem1  41286  hoidmvval0  41303  hoidmvlelem1  41311  vonioo  41398  vonicc  41401  smfaddlem1  41473  smfresal  41497  smfpimbor1lem2  41508  smflimmpt  41518  smfinflem  41525  smflimsuplem7  41534  smflimsuplem8  41535  smflimsupmpt  41537  smfliminfmpt  41540  ffnafv  41753  iccpartdisj  41879  mogoldbb  42179  2zrngagrp  42449  iunord  42928
  Copyright terms: Public domain W3C validator