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

Theorem rexlimddv 3253
 Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1 (𝜑 → ∃𝑥𝐴 𝜓)
rexlimddv.2 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
Assertion
Ref Expression
rexlimddv (𝜑𝜒)
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
2 rexlimddv.2 . . 3 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
32rexlimdvaa 3247 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  ∃wrex 3110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3114  df-rex 3115 This theorem is referenced by:  oaabs2  8259  oemapvali  9135  cantnflem4  9143  r1pwss  9201  djuun  9343  infxpenc2lem1  9434  pwfseqlem3  10075  prlem934  10448  ltexprlem7  10457  reclem3pr  10464  00id  10808  mul02lem1  10809  addid2  10816  addcan  10817  addcan2  10818  negeu  10869  mulcand  11266  suprzcl  12054  uzwo3  12335  expmulnbnd  13596  limsupgre  14833  rlimclim1  14897  fsumcvg3  15081  oexpneg  15689  bitsfi  15779  vdwlem10  16319  mreexexlem4d  16913  mreexdomd  16915  isacs3lem  17771  grprinvlem  17878  grpridd  17880  grprcan  18132  sylow1  18723  pgpfi  18725  slwhash  18744  pj1id  18820  efgsfo  18860  efgredlemc  18866  dmdprdsplitlem  19155  dpjidcl  19176  pgpfac1lem4  19196  pgpfaclem2  19200  pgpfaclem3  19201  ablsimpgcygd  19224  ablsimpgfindlem1  19225  ablsimpgfind  19228  fincygsubgodexd  19231  ablsimpgprmd  19233  gsummgp0  19357  lspsolv  19911  restbas  21766  restcls  21789  restntr  21790  cnpnei  21872  cnpco  21875  pnrmopn  21951  1stcfb  22053  1stcrest  22061  2ndcctbss  22063  2ndcomap  22066  dis2ndc  22068  llyidm  22096  nllyidm  22097  hausllycmp  22102  lly1stc  22104  llycmpkgen2  22158  1stckgenlem  22161  basqtop  22319  regr1lem  22347  kqreglem1  22349  kqreglem2  22350  kqnrmlem1  22351  kqnrmlem2  22352  reghmph  22401  nrmhmph  22402  qtophmeo  22425  trfbas2  22451  fbasfip  22476  fbasrn  22492  trfg  22499  ssufl  22526  fmufil  22567  ufldom  22570  uffclsflim  22639  cnpfcfi  22648  alexsublem  22652  alexsubALTlem4  22658  ptcmplem3  22662  ptcmplem4  22663  tsmsxp  22763  met1stc  23131  met2ndci  23132  prdsxmslem2  23139  metcnpi3  23156  icccmplem1  23430  xrge0tsms  23442  metdseq0  23462  cnllycmp  23564  bndth  23566  lebnumlem1  23569  lebnum  23572  cfilfcls  23881  lmle  23908  relcmpcmet  23925  pjthlem2  24045  ovolscalem2  24121  ovolicc2lem4  24127  ovolicc2lem5  24128  ioombl1  24169  uniioombllem6  24195  uniioombl  24196  opnmbllem  24208  volivth  24214  mbfinf  24272  mbfi1fseqlem6  24327  itg2cnlem1  24368  itg2cn  24370  lhop2  24621  dvcnvre  24625  aareccl  24925  aaliou3lem8  24944  aaliou3lem9  24949  ulmdvlem3  25000  mtestbdd  25003  iblulm  25005  radcnvlem1  25011  abelthlem5  25033  abelthlem8  25037  chordthm  25426  dcubic  25435  lgambdd  25625  lgamucov  25626  lgamcvglem  25628  lgamcvg2  25643  fta  25668  dchrptlem2  25852  sumdchr2  25857  2sqlem11  26016  dchrisum  26079  dchrisum0flb  26097  pntibndlem3  26179  pntlemi  26191  pjspansn  29363  chscllem3  29425  xmulcand  30626  xrge0tsmsd  30745  esumpcvgval  31445  cnpconn  32585  pconnconn  32586  connpconn  32590  pconnpi1  32592  cnllysconn  32600  cvmcov2  32630  cvmliftpht  32673  mthmpps  32937  sinccvg  33024  btwnconn1lem13  33668  neibastop2lem  33816  tailfb  33833  unblimceq0lem  33953  knoppndvlem9  33967  knoppndvlem21  33979  knoppndvlem22  33980  matunitlindflem2  35047  poimirlem29  35079  opnmbllem0  35086  mblfinlem2  35088  mblfinlem4  35090  prdsbnd2  35226  cntotbnd  35227  heiborlem8  35249  heiborlem9  35250  cvlcvr1  36628  llnmlplnN  36828  cdlemb  37083  paddasslem10  37118  trlcnv  37454  trlator0  37460  trlid0  37465  trlnidatb  37466  cdlemd4  37490  cdlemg5  37894  trlco  38016  cdlemj3  38112  tendo0mul  38115  tendo0mulr  38116  tendoconid  38118  erngdv  38282  erngdv-rN  38290  dihmeetlem1N  38579  dihatlat  38623  hgmaprnlem5N  39189  remulcan2d  39451  renegeulemv  39493  remul02  39530  remul01  39532  sn-addcand  39543  sn-addid1  39544  sn-addcan2d  39545  sn-subeu  39550  remulinvcom  39556  remulid2  39557  remulcand  39562  sn-0tie0  39563  itrere  39578  retire  39579  prjspertr  39586  0prjspnrel  39600  acongrep  39908  jm2.27b  39934  lmhmfgsplit  40017  hbt  40061  imo72b2lem1  40861  mnuss2d  40959  mnuprdlem4  40970  mnuunid  40972  mnurndlem2  40977  cncmpmax  41648  rexlimddv2  42452  stoweidlem62  42691  oexpnegALTV  44182  oexpnegnz  44183  aacllem  45316
 Copyright terms: Public domain W3C validator