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

Theorem rexlimd 3055
Description: Deduction form of rexlimd 3055. (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 3054 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1748  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-ral 2946  df-rex 2947
This theorem is referenced by:  r19.29af2  3104  reusv2lem2  4899  reusv2lem2OLD  4900  ralxfrALT  4917  fvmptt  6339  ffnfv  6428  peano5  7131  tz7.49  7585  nneneq  8184  ac6sfi  8245  ixpiunwdom  8537  r1val1  8687  rankuni2b  8754  infpssrlem4  9166  zorn2lem4  9359  zorn2lem5  9360  konigthlem  9428  tskuni  9643  gruiin  9670  lbzbi  11814  reuccats1  13526  fprodle  14771  iunconnlem  21278  ptbasfi  21432  alexsubALTlem3  21900  ovoliunnul  23321  iunmbl2  23371  mptelee  25820  atom1d  29340  elabreximd  29474  iundisjf  29528  esumc  30241  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  heicant  33574  indexa  33658  sdclem2  33668  glbconxN  34982  cdleme26ee  35965  cdleme32d  36049  cdleme32f  36051  cdlemk38  36520  cdlemk19x  36548  cdlemk11t  36551  refsumcn  39503  eliuniin2  39617  rexlimd3  39649  suprnmpt  39669  dffo3f  39678  wessf1ornlem  39685  disjf1o  39692  disjinfi  39694  funimassd  39745  rnmptlb  39767  rnmptbddlem  39769  fvelimad  39772  rnmptbd2lem  39777  infnsuprnmpt  39779  upbdrech  39833  ssfiunibd  39837  iuneqfzuzlem  39863  infrpge  39880  xrralrecnnle  39915  supxrleubrnmpt  39945  infleinf2  39954  suprleubrnmpt  39962  infrnmptle  39963  infxrunb3rnmpt  39968  infxrgelbrnmpt  39996  iccshift  40062  iooshift  40066  fmul01lt1  40136  islptre  40169  rexlim2d  40175  limcperiod  40178  islpcn  40189  limclner  40201  fnlimfvre  40224  climinf2lem  40256  limsupmnflem  40270  limsupre3uzlem  40285  climuzlem  40293  dvnprodlem1  40479  dvnprodlem2  40480  itgperiod  40515  stoweidlem29  40564  stoweidlem31  40566  stoweidlem59  40594  stirlinglem13  40621  fourierdlem48  40689  fourierdlem51  40692  fourierdlem53  40694  fourierdlem80  40721  fourierdlem81  40722  fourierdlem93  40734  elaa2  40769  salexct  40870  sge00  40911  sge0f1o  40917  sge0gerp  40930  sge0lefi  40933  sge0ltfirp  40935  sge0resplit  40941  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0isum  40962  sge0xp  40964  sge0reuz  40982  sge0reuzb  40983  iundjiun  40995  voliunsge0lem  41007  meaiuninc3v  41019  meaiininc2  41023  isomenndlem  41065  ovncvrrp  41099  ovnsubaddlem1  41105  hoidmvval0  41122  hoidmvlelem1  41130  vonioo  41217  vonicc  41220  smfaddlem1  41292  smfresal  41316  smfpimbor1lem2  41327  smflimmpt  41337  smfinflem  41344  smflimsuplem7  41353  smflimsuplem8  41354  smflimsupmpt  41356  smfliminfmpt  41359  ffnafv  41572  iccpartdisj  41698  mogoldbb  41998  2zrngagrp  42268  iunord  42747
  Copyright terms: Public domain W3C validator