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

Theorem rexlimddv 3223
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 3220 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2156  wrex 3097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-ral 3101  df-rex 3102
This theorem is referenced by:  grprinvlem  7098  grpridd  7100  oaabs2  7958  oemapvali  8824  cantnflem4  8832  r1pwss  8890  djuun  9031  infxpenc2lem1  9121  pwfseqlem3  9763  prlem934  10136  ltexprlem7  10145  reclem3pr  10152  00id  10492  mul02lem1  10493  addid2  10500  addcan  10501  addcan2  10502  negeu  10552  mulcand  10941  suprzcl  11719  uzwo3  11998  expmulnbnd  13215  limsupgre  14431  rlimclim1  14495  fsumcvg3  14679  oexpneg  15285  bitsfi  15374  vdwlem10  15907  mreexexlem4d  16508  mreexdomd  16510  isacs3lem  17367  grprcan  17656  sylow1  18215  pgpfi  18217  slwhash  18236  pj1id  18309  efgsfo  18349  efgredlemc  18355  dmdprdsplitlem  18634  dpjidcl  18655  pgpfac1lem4  18675  pgpfaclem2  18679  pgpfaclem3  18680  gsummgp0  18806  lspsolv  19347  restbas  21173  restcls  21196  restntr  21197  cnpnei  21279  cnpco  21282  pnrmopn  21358  1stcfb  21459  1stcrest  21467  2ndcctbss  21469  2ndcomap  21472  dis2ndc  21474  llyidm  21502  nllyidm  21503  hausllycmp  21508  lly1stc  21510  llycmpkgen2  21564  1stckgenlem  21567  basqtop  21725  regr1lem  21753  kqreglem1  21755  kqreglem2  21756  kqnrmlem1  21757  kqnrmlem2  21758  reghmph  21807  nrmhmph  21808  qtophmeo  21831  trfbas2  21857  fbasfip  21882  fbasrn  21898  trfg  21905  ssufl  21932  fmufil  21973  ufldom  21976  uffclsflim  22045  cnpfcfi  22054  alexsublem  22058  alexsubALTlem4  22064  ptcmplem3  22068  ptcmplem4  22069  tsmsxp  22168  met1stc  22536  met2ndci  22537  prdsxmslem2  22544  metcnpi3  22561  icccmplem1  22835  xrge0tsms  22847  metdseq0  22867  cnllycmp  22965  bndth  22967  lebnumlem1  22970  lebnum  22973  cfilfcls  23282  lmle  23309  relcmpcmet  23325  pjthlem2  23420  ovolscalem2  23494  ovolicc2lem4  23500  ovolicc2lem5  23501  ioombl1  23542  uniioombllem6  23568  uniioombl  23569  opnmbllem  23581  volivth  23587  mbfinf  23645  mbfi1fseqlem6  23700  itg2cnlem1  23741  itg2cn  23743  lhop2  23991  dvcnvre  23995  aareccl  24294  aaliou3lem8  24313  aaliou3lem9  24318  ulmdvlem3  24369  mtestbdd  24372  iblulm  24374  radcnvlem1  24380  abelthlem5  24402  abelthlem8  24406  chordthm  24777  dcubic  24786  lgambdd  24976  lgamucov  24977  lgamcvglem  24979  lgamcvg2  24994  fta  25019  dchrptlem2  25203  sumdchr2  25208  2sqlem11  25367  dchrisum  25394  dchrisum0flb  25412  pntibndlem3  25494  pntlemi  25506  pjspansn  28763  chscllem3  28825  xmulcand  29953  xrge0tsmsd  30109  esumpcvgval  30464  cnpconn  31533  pconnconn  31534  connpconn  31538  pconnpi1  31540  cnllysconn  31548  cvmcov2  31578  cvmliftpht  31621  mthmpps  31800  sinccvg  31887  btwnconn1lem13  32525  neibastop2lem  32674  tailfb  32691  unblimceq0lem  32812  knoppndvlem9  32826  knoppndvlem21  32838  knoppndvlem22  32839  matunitlindflem2  33717  poimirlem29  33749  opnmbllem0  33756  mblfinlem2  33758  mblfinlem4  33760  prdsbnd2  33903  cntotbnd  33904  heiborlem8  33926  heiborlem9  33927  cvlcvr1  35117  llnmlplnN  35317  cdlemb  35572  paddasslem10  35607  trlcnv  35943  trlator0  35949  trlid0  35954  trlnidatb  35955  cdlemd4  35979  cdlemg5  36383  trlco  36505  cdlemj3  36601  tendo0mul  36604  tendo0mulr  36605  tendoconid  36607  erngdv  36771  erngdv-rN  36779  dihmeetlem1N  37068  dihatlat  37112  hgmaprnlem5N  37678  acongrep  38045  jm2.27b  38071  lmhmfgsplit  38154  hbt  38198  imo72b2lem1  38968  cncmpmax  39682  rexlimddv2  40526  stoweidlem62  40755  oexpnegALTV  42160  oexpnegnz  42161  aacllem  43115
  Copyright terms: Public domain W3C validator