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

Theorem reximdva 2878
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 432 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2875 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1842   E.wrex 2754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-ral 2758  df-rex 2759
This theorem is referenced by:  reximddv  2879  reximddv2  2880  wereu2  4819  dffo4  6024  nnaordex  7323  frfi  7798  fisupg  7801  marypha1  7927  wemapsolem  8008  unwdomg  8043  rankr1ai  8247  cofsmo  8680  cfcoflem  8683  inar1  9182  nqerf  9337  prlem936  9454  fimaxre  10529  arch  10832  bndndx  10834  suprfinzcl  11017  zmin  11222  qbtwnxr  11451  qsqueeze  11452  qextltlem  11453  xrsupsslem  11550  xrinfmsslem  11551  xrub  11555  supxrunb1  11563  ssnn0fi  12133  fsuppmapnn0fiub0  12141  fsuppmapnn0fz  12144  expnlbnd2  12339  r19.29uz  13330  cau3lem  13334  rlim2lt  13467  rlimclim  13516  2clim  13542  o1co  13556  climcn1  13561  climcn2  13562  rlimo1  13586  climsqz  13610  climsqz2  13611  rlimsqzlem  13618  lo1le  13621  climsup  13639  climcau  13640  caucvgrlem2  13644  iseralt  13654  cvgcmp  13779  cvgcmpce  13781  supcvg  13817  rpnnen2  14166  bezoutlem1  14383  exprmfct  14458  pclem  14569  pc2dvds  14609  pcprmpw  14613  unbenlem  14633  infpnlem2  14636  infpn2  14638  prmunb  14639  vdwlem2  14707  ramub1lem2  14752  ipodrsima  16117  grpinveu  16406  psgneu  16853  odbezout  16902  sylow2blem3  16964  nn0gsumfz  17330  irredrmul  17674  lsmelval2  18049  lbsextlem2  18123  mptcoe1fsupp  18573  znunit  18898  scmate  19302  scmatscm  19305  scmatfo  19322  mat1scmat  19331  pmatcoe1fsupp  19492  pmatcollpwfi  19573  pmatcollpw3fi  19576  mptcoe1matfsupp  19593  pm2mp  19616  chmaidscmat  19639  cpmadugsum  19669  cpmadumatpoly  19674  chcoeffeq  19677  cayhamlem3  19678  cayhamlem4  19679  neiptopnei  19924  neitr  19972  cnpnei  20056  haust1  20144  isnrm3  20151  isreg2  20169  tgcmp  20192  hauscmplem  20197  hauscmp  20198  bwth  20201  1stcfb  20236  1stcelcls  20252  lly1stc  20287  txcmplem1  20432  txlm  20439  xkococnlem  20450  filuni  20676  filufint  20711  ufilen  20721  fclscf  20816  cnextcn  20857  ustex2sym  21009  ustex3sym  21010  utopreg  21045  isucn2  21072  ucnima  21074  ucncn  21078  neipcfilu  21089  metequiv2  21303  metrest  21317  xrsmopn  21607  mulc1cncf  21699  cncfco  21701  bndth  21748  lmmcvg  21990  cfil3i  21998  iscau4  22008  cmetcaulem  22017  iscmet3lem1  22020  caussi  22026  equivcfil  22028  equivcau  22029  caubl  22036  minveclem3b  22133  ovolgelb  22181  ovollb2lem  22189  ovolctb  22191  ovolicc2lem4  22221  ioombl1lem4  22261  dyadmax  22297  volsup2  22304  itg2monolem1  22447  c1liplem1  22687  c1lip1  22688  dvivthlem1  22699  lhop1  22705  ftc1a  22728  ftc1lem6  22732  ply1divex  22827  elply2  22883  dgrlem  22916  aacjcl  23013  aalioulem2  23019  aalioulem3  23020  aalioulem4  23021  ulmcaulem  23079  ulmcau  23080  ulmss  23082  mtest  23089  itgulm  23093  reeff1o  23132  efif1olem4  23222  rlimcnp  23619  xrlimcnp  23622  lgamucov  23691  ftalem3  23727  fta  23732  muval1  23786  dvdssqf  23791  mumullem1  23832  pntlem3  24173  ostth  24203  tgtrisegint  24269  tgbtwndiff  24276  tgcgrxfr  24288  lnext  24335  legov2  24354  legtrd  24357  hlcgrex  24381  colperpexlem3  24489  colperpex  24490  hpgerlem  24517  hpgtr  24520  dfcgra2  24566  axpasch  24648  wwlknredwwlkn0  25131  2pthfrgrarn2  25414  frgrawopreglem5  25452  usgreg2spot  25471  grpoidinvlem3  25608  grpoideu  25611  grpoinveu  25624  isgrp2d  25637  rngo2  25790  ubthlem1  26186  minvecolem5  26197  htthlem  26234  chscllem2  26956  nmopun  27332  lnconi  27351  rnbra  27425  sumdmdii  27733  cdj3lem2b  27755  foresf1o  27804  acunirnmpt  27929  xrofsup  28016  isarchi3  28169  isarchiofld  28246  lmxrge0  28373  lmdvg  28374  esumlub  28493  esumfsup  28503  esumcvg  28519  eulerpartlemgvv  28807  cvmliftmolem2  29566  cvmlift2lem10  29596  cvmlift2lem12  29598  frmin  30040  wzel  30067  wsuclem  30068  nofulllem5  30153  btwndiff  30352  trisegint  30353  cgrxfr  30380  lineext  30401  segcon2  30430  brsegle2  30434  seglecgr12im  30435  segletr  30439  broutsideof3  30451  opnrebl2  30536  nn0prpw  30538  fin2so  31392  mblfinlem1  31403  mblfinlem2  31404  mblfinlem3  31405  mblfinlem4  31406  itg2addnclem  31419  ftc1cnnc  31442  ftc1anclem5  31447  ftc1anclem6  31448  sdclem1  31498  geomcau  31514  equivtotbnd  31536  bndss  31544  ismtybndlem  31564  heibor1lem  31567  rrncmslem  31590  prtlem15  31878  lsateln0  31993  lsat0cv  32031  eqlkr3  32099  lkrshp  32103  lshpset2N  32117  hlhgt2  32386  hlrelat2  32400  atle  32433  athgt  32453  2dim  32467  1cvratex  32470  ps-2  32475  dalem20  32690  lhpexle1lem  33004  lhpexle1  33005  lhpexle2lem  33006  lhpmcvr5N  33024  lhpmcvr6N  33025  cdleme25a  33352  cdleme29ex  33373  cdlemfnid  33563  cdlemg33b0  33700  cdlemg33a  33705  cdlemg35  33712  cdleml3N  33977  dihlsscpre  34234  dih1dimb2  34241  dihatexv  34338  dvh3dim2  34448  dochkr1  34478  dochkr1OLDN  34479  lcfl8  34502  lcfl8b  34504  lcfrlem5  34546  lcfrlem6  34547  mapdrvallem2  34645  mapdh9a  34790  mapdh9aOLDN  34791  hdmaprnlem3eN  34861  hdmaprnlem16N  34865  fphpdo  35092  rencldnfilem  35095  irrapxlem2  35100  cvgdvgrat  36022  lcmgcdlem  36040  expgrowth  36068  ssfiunibd  36858  climinf  36961  mullimc  36971  islptre  36974  limccog  36975  mullimcf  36978  limcrecl  36984  sumnnodd  36985  neglimc  37002  0ellimcdiv  37004  limclner  37006  cncfioobd  37049  stoweidlem7  37138  stoweidlem27  37158  stoweidlem39  37170  stoweidlem48  37179  stoweidlem49  37180  stoweidlem60  37191  stoweidlem61  37192  stoweid  37194  dirkercncflem2  37235  fourierdlem20  37258  fourierdlem39  37277  fourierdlem41  37279  fourierdlem48  37286  fourierdlem49  37287  fourierdlem50  37288  fourierdlem64  37302  fourierdlem73  37311  fourierdlem74  37312  fourierdlem75  37313  fourierdlem87  37325  fourierdlem103  37341  fourierdlem104  37342  bgoldbwt  37812  bgoldbst  37813  sgoldbalt  37816  bgoldbtbndlem4  37837  bgoldbtbnd  37838  proththd  37841  zrninitoringc  38371  ply1mulgsumlem3  38480  ply1mulgsumlem4  38481  islindeps2  38576  isldepslvec2  38578
  Copyright terms: Public domain W3C validator