MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximdva Unicode version

Theorem reximdva 2626
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
reximdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
reximdva  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem reximdva
StepHypRef Expression
1 reximdva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21ex 425 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2624 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  wereu2  4327  dffo4  5575  nnaordex  6569  frfi  7035  fisupg  7038  marypha1  7120  wemapso2lem  7198  unwdomg  7231  noinfepOLD  7294  rankr1ai  7403  cofsmo  7828  cfcoflem  7831  inar1  8330  nqerf  8487  prlem936  8604  fimaxre  9634  arch  9894  bndndx  9896  zmin  10244  qbtwnxr  10458  qsqueeze  10459  qextltlem  10460  xrsupsslem  10556  xrinfmsslem  10557  xrub  10561  supxrunb1  10569  expnlbnd2  11163  r19.29uz  11764  cau3lem  11768  rlim2lt  11901  rlimclim  11950  2clim  11976  o1co  11990  climcn1  11995  climcn2  11996  rlimo1  12020  climsqz  12044  climsqz2  12045  rlimsqzlem  12052  lo1le  12055  climsup  12073  climcau  12074  caucvgrlem  12075  caucvgrlem2  12077  iseralt  12087  cvgcmp  12204  cvgcmpce  12206  supcvg  12241  rpnnen2  12431  bezoutlem1  12644  exprmfct  12716  isprm5  12718  pclem  12818  pc2dvds  12858  pcprmpw  12862  unbenlem  12882  infpnlem2  12885  infpn2  12887  prmunb  12888  vdwlem2  12956  ramub1lem2  13001  drsdirfi  13999  ipodrsima  14195  grpinveu  14443  odbezout  14798  sylow2blem3  14860  sylow2  14864  gexex  15072  irredrmul  15416  lsmelval2  15765  lbsextlem2  15839  znunit  16444  cnpnei  16920  haust1  17007  nrmsep  17012  isnrm3  17014  regsep2  17031  isreg2  17032  tgcmp  17055  hauscmplem  17060  hauscmp  17061  1stcfb  17098  1stcelcls  17114  lly1stc  17149  txcmplem1  17262  txlm  17269  xkococnlem  17280  filuni  17507  filufint  17542  ufilen  17552  fclscf  17647  metequiv2  17983  met1stc  17994  metrest  17997  xrsmopn  18245  xrge0tsms  18266  mulc1cncf  18336  cncfco  18338  cnheibor  18380  bndth  18383  lmmcvg  18614  cfil3i  18622  iscau4  18632  cmetcaulem  18641  iscmet3lem1  18644  caussi  18650  equivcfil  18652  equivcau  18653  caubl  18660  lmcau  18665  minveclem3b  18719  ovolgelb  18766  ovollb2lem  18774  ovolctb  18776  ovolicc2lem4  18806  ioombl1lem4  18845  dyadmax  18880  volsup2  18887  ismbf3d  18936  itg2monolem1  19032  c1liplem1  19270  c1lip1  19271  dvivthlem1  19282  lhop1  19288  ftc1a  19311  ftc1lem6  19315  ply1divex  19449  elply2  19505  dgrlem  19538  aacjcl  19634  aalioulem2  19640  aalioulem3  19641  aalioulem4  19642  ulmcaulem  19698  ulmcau  19699  ulmss  19701  ulmdvlem3  19706  mtest  19708  itgulm  19711  reeff1o  19750  efif1olem4  19834  rlimcnp  20187  xrlimcnp  20190  ftalem3  20239  fta  20244  muval1  20298  dvdssqf  20303  mumullem1  20344  pntlem3  20685  ostth  20715  grpoidinvlem3  20798  grpoideu  20801  grpoinveu  20814  isgrp2d  20827  rngo2  20980  ubthlem1  21374  minvecolem5  21385  htthlem  21422  pjhthlem2  21896  chscllem2  22160  nmopun  22519  lnconi  22538  rnbra  22612  sumdmdii  22920  cdj3lem2b  22942  reximddv  22953  cvmliftmolem2  23150  cvmliftlem15  23166  cvmlift2lem10  23180  cvmlift2lem12  23182  dedekind  23418  frmin  23576  axfelem18  23697  axfelem22  23701  axpasch  23909  btwndiff  23990  trisegint  23991  cgrxfr  24018  lineext  24039  segcon2  24068  brsegle2  24072  seglecgr12im  24073  segletr  24077  broutsideof3  24089  pdiveql  25500  abhp  25505  opnrebl2  25568  nn0prpw  25571  locfincmp  25636  sdclem1  25785  geomcau  25807  equivtotbnd  25834  bndss  25842  ismtybndlem  25862  heibor1lem  25865  rrncmslem  25888  prtlem15  26075  nacsfix  26119  fphpdo  26232  rencldnfilem  26235  irrapxlem2  26240  unxpwdom3  26588  psgneu  26761  expgrowth  26884  stoweidlem7  27056  stoweidlem27  27076  stoweidlem39  27088  stoweidlem48  27097  stoweidlem49  27098  stoweidlem60  27109  stoweidlem61  27110  stoweid  27112  lsateln0  28315  lsat0cv  28353  eqlkr3  28421  lkrshp  28425  lshpset2N  28439  hlhgt2  28708  hlrelat2  28722  atle  28755  athgt  28775  2dim  28789  1cvratex  28792  ps-2  28797  dalem20  29012  lhpexle1lem  29326  lhpexle1  29327  lhpexle2lem  29328  lhpmcvr5N  29346  lhpmcvr6N  29347  cdleme25a  29672  cdleme29ex  29693  cdlemfnid  29883  cdlemg33b0  30020  cdlemg33a  30025  cdlemg35  30032  cdleml3N  30297  dihlsscpre  30554  dih1dimb2  30561  dihatexv  30658  dvh3dim2  30768  dochkr1  30798  dochkr1OLDN  30799  lcfl8  30822  lcfl8b  30824  lcfrlem5  30866  lcfrlem6  30867  mapdrvallem2  30965  mapdh9a  31110  mapdh9aOLDN  31111  hdmaprnlem3eN  31181  hdmaprnlem16N  31185
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2520  df-rex 2521
  Copyright terms: Public domain W3C validator