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

Theorem reximdva 2938
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 434 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2935 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  reximddv  2939  reximddv2  2940  wereu2  4876  dffo4  6037  nnaordex  7287  frfi  7765  fisupg  7768  marypha1  7894  wemapsolem  7975  unwdomg  8010  noinfepOLD  8077  rankr1ai  8216  cofsmo  8649  cfcoflem  8652  inar1  9153  nqerf  9308  prlem936  9425  dedekind  9743  fimaxre  10490  arch  10792  bndndx  10794  suprfinzcl  10975  zmin  11178  qbtwnxr  11399  qsqueeze  11400  qextltlem  11401  xrsupsslem  11498  xrinfmsslem  11499  xrub  11503  supxrunb1  11511  ssnn0fi  12062  fsuppmapnn0fiub0  12067  fsuppmapnn0fz  12070  expnlbnd2  12265  r19.29uz  13146  cau3lem  13150  rlim2lt  13283  rlimclim  13332  2clim  13358  o1co  13372  climcn1  13377  climcn2  13378  rlimo1  13402  climsqz  13426  climsqz2  13427  rlimsqzlem  13434  lo1le  13437  climsup  13455  climcau  13456  caucvgrlem  13458  caucvgrlem2  13460  iseralt  13470  cvgcmp  13593  cvgcmpce  13595  supcvg  13630  rpnnen2  13820  bezoutlem1  14035  exprmfct  14110  isprm5  14112  pclem  14221  pc2dvds  14261  pcprmpw  14265  unbenlem  14285  infpnlem2  14288  infpn2  14290  prmunb  14291  vdwlem2  14359  ramub1lem2  14404  drsdirfi  15425  ipodrsima  15652  grpinveu  15894  psgneu  16337  odbezout  16386  sylow2blem3  16448  sylow2  16452  gexex  16662  nn0gsumfz  16815  irredrmul  17157  lsmelval2  17531  lbsextlem2  17605  mptcoe1fsupp  18054  znunit  18397  scmate  18807  scmatscm  18810  scmatfo  18827  mat1scmat  18836  pmatcoe1fsupp  18997  pmatcollpwfi  19078  pmatcollpw3fi  19081  mptcoe1matfsupp  19098  pm2mp  19121  chmaidscmat  19144  cpmadugsumfi  19173  cpmadugsum  19174  cpmidg2sum  19176  cpmadumatpoly  19179  chcoeffeq  19182  cayhamlem3  19183  cayhamlem4  19184  neiptopnei  19427  neitr  19475  cnpnei  19559  haust1  19647  nrmsep  19652  isnrm3  19654  regsep2  19671  isreg2  19672  tgcmp  19695  hauscmplem  19700  hauscmp  19701  bwth  19704  1stcfb  19740  1stcelcls  19756  lly1stc  19791  txcmplem1  19905  txlm  19912  xkococnlem  19923  filuni  20149  filufint  20184  ufilen  20194  fclscf  20289  cnextcn  20330  ustex2sym  20482  ustex3sym  20483  utopreg  20518  isucn2  20545  ucnima  20547  ucncn  20551  neipcfilu  20562  metequiv2  20776  met1stc  20787  metrest  20790  xrsmopn  21080  mulc1cncf  21172  cncfco  21174  cnheibor  21218  bndth  21221  lmmcvg  21463  cfil3i  21471  iscau4  21481  cmetcaulem  21490  iscmet3lem1  21493  caussi  21499  equivcfil  21501  equivcau  21502  caubl  21509  lmcau  21514  minveclem3b  21606  ovolgelb  21654  ovollb2lem  21662  ovolctb  21664  ovolicc2lem4  21694  ioombl1lem4  21734  dyadmax  21770  volsup2  21777  ismbf3d  21824  itg2monolem1  21920  c1liplem1  22160  c1lip1  22161  dvivthlem1  22172  lhop1  22178  ftc1a  22201  ftc1lem6  22205  ply1divex  22300  elply2  22356  dgrlem  22389  aacjcl  22485  aalioulem2  22491  aalioulem3  22492  aalioulem4  22493  ulmcaulem  22551  ulmcau  22552  ulmss  22554  ulmdvlem3  22559  mtest  22561  itgulm  22565  reeff1o  22604  efif1olem4  22693  rlimcnp  23051  xrlimcnp  23054  ftalem3  23104  fta  23109  muval1  23163  dvdssqf  23168  mumullem1  23209  pntlem3  23550  ostth  23580  tgtrisegint  23646  tgbtwndiff  23653  tgcgrxfr  23665  lnext  23709  legov2  23728  legtrd  23731  colperpexlem3  23839  colperpex  23840  axpasch  23948  wwlknredwwlkn0  24431  2pthfrgrarn2  24714  frgrawopreglem5  24753  usgreg2spot  24772  grpoidinvlem3  24912  grpoideu  24915  grpoinveu  24928  isgrp2d  24941  rngo2  25094  ubthlem1  25490  minvecolem5  25501  htthlem  25538  pjhthlem2  26014  chscllem2  26260  nmopun  26637  lnconi  26656  rnbra  26730  sumdmdii  27038  cdj3lem2b  27060  xrofsup  27278  isarchi3  27421  isarchiofld  27498  lmxrge0  27598  lmdvg  27599  esumlub  27736  esumfsup  27744  esumcvg  27760  eulerpartlemgvv  27983  lgamucov  28248  cvmliftmolem2  28395  cvmliftlem15  28411  cvmlift2lem10  28425  cvmlift2lem12  28427  frmin  28927  wzel  28985  wsuclem  28986  nofulllem5  29071  btwndiff  29282  trisegint  29283  cgrxfr  29310  lineext  29331  segcon2  29360  brsegle2  29364  seglecgr12im  29365  segletr  29369  broutsideof3  29381  fin2so  29645  mblfinlem1  29656  mblfinlem2  29657  mblfinlem3  29658  mblfinlem4  29659  itg2addnclem  29671  ftc1cnnc  29694  ftc1anclem5  29699  ftc1anclem6  29700  opnrebl2  29744  nn0prpw  29746  locfincmp  29804  sdclem1  29867  geomcau  29883  equivtotbnd  29905  bndss  29913  ismtybndlem  29933  heibor1lem  29936  rrncmslem  29959  prtlem15  30248  nacsfix  30276  fphpdo  30383  rencldnfilem  30386  irrapxlem2  30391  unxpwdom3  30673  lcmgcdlem  30840  expgrowth  30868  ssfiunibd  31114  climinf  31176  mullimc  31186  islptre  31189  limccog  31190  mullimcf  31193  limcrecl  31199  sumnnodd  31200  neglimc  31217  limclner  31221  cncfioobd  31264  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  stoweidlem7  31335  stoweidlem27  31355  stoweidlem39  31367  stoweidlem48  31376  stoweidlem49  31377  stoweidlem60  31388  stoweidlem61  31389  stoweid  31391  dirkercncflem2  31432  fourierdlem20  31455  fourierdlem39  31474  fourierdlem41  31476  fourierdlem48  31483  fourierdlem49  31484  fourierdlem50  31485  fourierdlem64  31499  fourierdlem73  31508  fourierdlem74  31509  fourierdlem75  31510  fourierdlem87  31522  fourierdlem103  31538  fourierdlem104  31539  ply1mulgsumlem3  32087  ply1mulgsumlem4  32088  islindeps2  32183  isldepslvec2  32185  lsateln0  33810  lsat0cv  33848  eqlkr3  33916  lkrshp  33920  lshpset2N  33934  hlhgt2  34203  hlrelat2  34217  atle  34250  athgt  34270  2dim  34284  1cvratex  34287  ps-2  34292  dalem20  34507  lhpexle1lem  34821  lhpexle1  34822  lhpexle2lem  34823  lhpmcvr5N  34841  lhpmcvr6N  34842  cdleme25a  35167  cdleme29ex  35188  cdlemfnid  35378  cdlemg33b0  35515  cdlemg33a  35520  cdlemg35  35527  cdleml3N  35792  dihlsscpre  36049  dih1dimb2  36056  dihatexv  36153  dvh3dim2  36263  dochkr1  36293  dochkr1OLDN  36294  lcfl8  36317  lcfl8b  36319  lcfrlem5  36361  lcfrlem6  36362  mapdrvallem2  36460  mapdh9a  36605  mapdh9aOLDN  36606  hdmaprnlem3eN  36676  hdmaprnlem16N  36680
  Copyright terms: Public domain W3C validator