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

Theorem rexlimd 3008
Description: Deduction form of rexlimd 3008. (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 3007 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1699  wcel 1977  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902
This theorem is referenced by:  r19.29af2  3057  reusv2lem2  4795  reusv2lem2OLD  4796  ralxfrALT  4813  fvmptt  6208  ffnfv  6295  peano5  6981  tz7.49  7427  nneneq  8028  ac6sfi  8089  ixpiunwdom  8379  r1val1  8532  rankuni2b  8599  infpssrlem4  9011  zorn2lem4  9204  zorn2lem5  9205  konigthlem  9269  tskuni  9484  gruiin  9511  lbzbi  11652  fprodle  14566  iunconlem  21040  ptbasfi  21194  alexsubALTlem3  21663  ovoliunnul  23082  iunmbl2  23132  mptelee  25575  atom1d  28596  elabreximd  28732  iundisjf  28784  esumc  29440  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  heicant  32614  indexa  32698  sdclem2  32708  glbconxN  33682  cdleme26ee  34666  cdleme32d  34750  cdleme32f  34752  cdlemk38  35221  cdlemk19x  35249  cdlemk11t  35252  refsumcn  38212  eliuniin2  38335  suprnmpt  38350  dffo3f  38359  wessf1ornlem  38366  disjf1o  38373  disjinfi  38375  upbdrech  38460  ssfiunibd  38464  iuneqfzuzlem  38491  infrpge  38508  xrralrecnnle  38543  iccshift  38591  iooshift  38595  fmul01lt1  38653  islptre  38686  rexlim2d  38692  limcperiod  38695  islpcn  38706  limclner  38718  fnlimfvre  38741  dvnprodlem1  38836  dvnprodlem2  38837  itgperiod  38873  stoweidlem29  38922  stoweidlem31  38924  stoweidlem59  38952  stirlinglem13  38979  fourierdlem48  39047  fourierdlem51  39050  fourierdlem53  39052  fourierdlem80  39079  fourierdlem81  39080  fourierdlem93  39092  elaa2  39127  salexct  39228  sge00  39269  sge0f1o  39275  sge0gerp  39288  sge0lefi  39291  sge0ltfirp  39293  sge0resplit  39299  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0isum  39320  sge0xp  39322  sge0reuz  39340  sge0reuzb  39341  iundjiun  39353  voliunsge0lem  39365  meaiininc2  39378  isomenndlem  39420  ovncvrrp  39454  ovnsubaddlem1  39460  hoidmvval0  39477  hoidmvlelem1  39485  vonioo  39573  vonicc  39576  smfaddlem1  39649  smfresal  39673  smfpimbor1lem2  39684  ffnafv  39900  iccpartdisj  39975  2zrngagrp  41733  iunord  42220
  Copyright terms: Public domain W3C validator