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

Theorem reximdva 2782
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 424 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2780 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   E.wrex 2671
This theorem is referenced by:  wereu2  4543  dffo4  5848  nnaordex  6844  frfi  7315  fisupg  7318  marypha1  7401  wemapso2lem  7479  unwdomg  7512  noinfepOLD  7575  rankr1ai  7684  cofsmo  8109  cfcoflem  8112  inar1  8610  nqerf  8767  prlem936  8884  fimaxre  9915  arch  10178  bndndx  10180  zmin  10530  qbtwnxr  10746  qsqueeze  10747  qextltlem  10748  xrsupsslem  10845  xrinfmsslem  10846  xrub  10850  supxrunb1  10858  expnlbnd2  11469  r19.29uz  12113  cau3lem  12117  rlim2lt  12250  rlimclim  12299  2clim  12325  o1co  12339  climcn1  12344  climcn2  12345  rlimo1  12369  climsqz  12393  climsqz2  12394  rlimsqzlem  12401  lo1le  12404  climsup  12422  climcau  12423  caucvgrlem  12425  caucvgrlem2  12427  iseralt  12437  cvgcmp  12554  cvgcmpce  12556  supcvg  12594  rpnnen2  12784  bezoutlem1  12997  exprmfct  13069  isprm5  13071  pclem  13171  pc2dvds  13211  pcprmpw  13215  unbenlem  13235  infpnlem2  13238  infpn2  13240  prmunb  13241  vdwlem2  13309  ramub1lem2  13354  drsdirfi  14354  ipodrsima  14550  grpinveu  14798  odbezout  15153  sylow2blem3  15215  sylow2  15219  gexex  15427  irredrmul  15771  lsmelval2  16116  lbsextlem2  16190  znunit  16803  neiptopnei  17155  neitr  17202  cnpnei  17286  haust1  17374  nrmsep  17379  isnrm3  17381  regsep2  17398  isreg2  17399  tgcmp  17422  hauscmplem  17427  hauscmp  17428  1stcfb  17465  1stcelcls  17481  lly1stc  17516  txcmplem1  17630  txlm  17637  xkococnlem  17648  filuni  17874  filufint  17909  ufilen  17919  fclscf  18014  cnextcn  18055  ustex2sym  18203  ustex3sym  18204  utopreg  18239  isucn2  18266  ucnima  18268  ucncn  18272  neipcfilu  18283  metequiv2  18497  met1stc  18508  metrest  18511  xrsmopn  18800  xrge0tsms  18822  mulc1cncf  18892  cncfco  18894  cnheibor  18937  bndth  18940  lmmcvg  19171  cfil3i  19179  iscau4  19189  cmetcaulem  19198  iscmet3lem1  19201  caussi  19207  equivcfil  19209  equivcau  19210  caubl  19217  lmcau  19222  minveclem3b  19286  ovolgelb  19333  ovollb2lem  19341  ovolctb  19343  ovolicc2lem4  19373  ioombl1lem4  19412  dyadmax  19447  volsup2  19454  ismbf3d  19503  itg2monolem1  19599  c1liplem1  19837  c1lip1  19838  dvivthlem1  19849  lhop1  19855  ftc1a  19878  ftc1lem6  19882  ply1divex  20016  elply2  20072  dgrlem  20105  aacjcl  20201  aalioulem2  20207  aalioulem3  20208  aalioulem4  20209  ulmcaulem  20267  ulmcau  20268  ulmss  20270  ulmdvlem3  20275  mtest  20277  itgulm  20281  reeff1o  20320  efif1olem4  20404  rlimcnp  20761  xrlimcnp  20764  ftalem3  20814  fta  20819  muval1  20873  dvdssqf  20878  mumullem1  20919  pntlem3  21260  ostth  21290  grpoidinvlem3  21751  grpoideu  21754  grpoinveu  21767  isgrp2d  21780  rngo2  21933  ubthlem1  22329  minvecolem5  22340  htthlem  22377  pjhthlem2  22851  chscllem2  23097  nmopun  23474  lnconi  23493  rnbra  23567  sumdmdii  23875  cdj3lem2b  23897  reximddv  23919  xrofsup  24083  lmxrge0  24294  lmdvg  24295  esumlub  24409  esumfsup  24417  esumcvg  24433  lgamucov  24779  cvmliftmolem2  24926  cvmliftlem15  24942  cvmlift2lem10  24956  cvmlift2lem12  24958  dedekind  25144  frmin  25460  nofulllem5  25578  axpasch  25788  btwndiff  25869  trisegint  25870  cgrxfr  25897  lineext  25918  segcon2  25947  brsegle2  25951  seglecgr12im  25952  segletr  25956  broutsideof3  25968  mblfinlem  26147  mblfinlem2  26148  mblfinlem3  26149  itg2addnclem  26159  ftc1cnnc  26182  opnrebl2  26218  nn0prpw  26220  locfincmp  26278  sdclem1  26341  geomcau  26359  equivtotbnd  26381  bndss  26389  ismtybndlem  26409  heibor1lem  26412  rrncmslem  26435  prtlem15  26618  nacsfix  26660  fphpdo  26772  rencldnfilem  26775  irrapxlem2  26780  unxpwdom3  27128  psgneu  27301  expgrowth  27424  climinf  27603  stoweidlem7  27627  stoweidlem27  27647  stoweidlem39  27659  stoweidlem48  27668  stoweidlem49  27669  stoweidlem60  27680  stoweidlem61  27681  stoweid  27683  2pthfrgrarn2  28118  frgrawopreglem5  28155  usgreg2spot  28174  lsateln0  29482  lsat0cv  29520  eqlkr3  29588  lkrshp  29592  lshpset2N  29606  hlhgt2  29875  hlrelat2  29889  atle  29922  athgt  29942  2dim  29956  1cvratex  29959  ps-2  29964  dalem20  30179  lhpexle1lem  30493  lhpexle1  30494  lhpexle2lem  30495  lhpmcvr5N  30513  lhpmcvr6N  30514  cdleme25a  30839  cdleme29ex  30860  cdlemfnid  31050  cdlemg33b0  31187  cdlemg33a  31192  cdlemg35  31199  cdleml3N  31464  dihlsscpre  31721  dih1dimb2  31728  dihatexv  31825  dvh3dim2  31935  dochkr1  31965  dochkr1OLDN  31966  lcfl8  31989  lcfl8b  31991  lcfrlem5  32033  lcfrlem6  32034  mapdrvallem2  32132  mapdh9a  32277  mapdh9aOLDN  32278  hdmaprnlem3eN  32348  hdmaprnlem16N  32352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2675  df-rex 2676
  Copyright terms: Public domain W3C validator