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

Theorem reximdva 2861
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 436 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2858 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1886   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-ral 2741  df-rex 2742
This theorem is referenced by:  reximddv  2862  reximddv2  2863  wereu2  4830  dffo4  6036  nnaordex  7336  frfi  7813  fisupg  7816  marypha1  7945  fiinfg  8012  wemapsolem  8062  unwdomg  8096  rankr1ai  8266  cofsmo  8696  cfcoflem  8699  inar1  9197  nqerf  9352  prlem936  9469  fimaxre  10548  arch  10863  bndndx  10865  suprfinzcl  11047  zmin  11257  qbtwnxr  11490  qsqueeze  11491  qextltlem  11492  xrsupsslem  11589  xrinfmsslem  11590  xrub  11594  supxrunb1  11602  ssnn0fi  12194  fsuppmapnn0fiub0  12202  fsuppmapnn0fz  12205  expnlbnd2  12400  r19.29uz  13406  cau3lem  13410  rlim2lt  13554  rlimclim  13603  2clim  13629  o1co  13643  climcn1  13648  climcn2  13649  rlimo1  13673  climsqz  13697  climsqz2  13698  rlimsqzlem  13705  lo1le  13708  climsup  13726  climcau  13727  caucvgrlem2  13733  iseralt  13744  cvgcmp  13869  cvgcmpce  13871  supcvg  13907  rpnnen2  14271  bezoutlem1  14496  lcmgcdlem  14564  exprmfct  14641  prmdvdsfz  14642  pclem  14781  pc2dvds  14821  pcprmpw  14825  unbenlem  14845  infpnlem2  14848  infpn2  14850  prmunb  14851  vdwlem2  14925  ramub1lem2  14978  prmdvdsprmop  14994  prmdvdsprmorpOLD  15009  prmgaplem7  15020  ipodrsima  16404  grpinveu  16693  psgneu  17140  odbezout  17202  sylow2blem3  17267  nn0gsumfz  17606  irredrmul  17928  lsmelval2  18301  lbsextlem2  18375  mptcoe1fsupp  18801  znunit  19127  scmate  19528  scmatscm  19531  scmatfo  19548  mat1scmat  19557  pmatcoe1fsupp  19718  pmatcollpwfi  19799  pmatcollpw3fi  19802  mptcoe1matfsupp  19819  pm2mp  19842  chmaidscmat  19865  cpmadugsum  19895  cpmadumatpoly  19900  chcoeffeq  19903  cayhamlem3  19904  cayhamlem4  19905  neiptopnei  20141  neitr  20189  cnpnei  20273  haust1  20361  isnrm3  20368  isreg2  20386  tgcmp  20409  hauscmplem  20414  hauscmp  20415  bwth  20418  1stcfb  20453  1stcelcls  20469  lly1stc  20504  txcmplem1  20649  txlm  20656  xkococnlem  20667  filuni  20893  filufint  20928  ufilen  20938  fclscf  21033  cnextcn  21075  ustex2sym  21224  ustex3sym  21225  utopreg  21260  isucn2  21287  ucnima  21289  ucncn  21293  neipcfilu  21304  metequiv2  21518  metrest  21532  xrsmopn  21823  mulc1cncf  21930  cncfco  21932  bndth  21979  lmmcvg  22224  cfil3i  22232  iscau4  22242  cmetcaulem  22251  iscmet3lem1  22254  caussi  22260  equivcfil  22262  equivcau  22263  caubl  22270  minveclem3b  22363  minveclem3bOLD  22375  ovolgelb  22426  ovollb2lem  22434  ovolctb  22436  ovolicc2lem4OLD  22466  ovolicc2lem4  22467  ioombl1lem4  22507  dyadmax  22549  volsup2  22556  itg2monolem1  22701  c1liplem1  22941  c1lip1  22942  dvivthlem1  22953  lhop1  22959  ftc1a  22982  ftc1lem6  22986  ply1divex  23080  elply2  23143  dgrlem  23176  aacjcl  23276  aalioulem2  23282  aalioulem3  23283  aalioulem4  23284  ulmcaulem  23342  ulmcau  23343  ulmss  23345  mtest  23352  itgulm  23356  reeff1o  23395  efif1olem4  23487  rlimcnp  23884  xrlimcnp  23887  lgamucov  23956  ftalem3  23992  fta  23999  muval1  24053  dvdssqf  24058  mumullem1  24099  pntlem3  24440  ostth  24470  tgtrisegint  24536  tgbtwndiff  24543  tgcgrxfr  24556  lnext  24605  legov2  24624  legtrd  24627  hlcgrex  24654  colperpexlem3  24767  colperpex  24768  hlpasch  24791  hpgerlem  24800  hpgtr  24803  dfcgra2  24864  acopy  24867  inagswap  24873  inaghl  24874  cgrg3col4  24877  axpasch  24964  wwlknredwwlkn0  25448  2pthfrgrarn2  25731  frgrawopreglem5  25769  usgreg2spot  25788  grpoidinvlem3  25927  grpoideu  25930  grpoinveu  25943  isgrp2d  25956  rngo2  26109  ubthlem1  26505  minvecolem5  26516  minvecolem5OLD  26526  htthlem  26563  chscllem2  27284  nmopun  27660  lnconi  27679  rnbra  27753  sumdmdii  28061  cdj3lem2b  28083  foresf1o  28132  acunirnmpt  28254  xrofsup  28346  isarchi3  28497  isarchiofld  28573  lmxrge0  28751  lmdvg  28752  esumlub  28874  esumfsup  28884  esumcvg  28900  eulerpartlemgvv  29202  cvmliftmolem2  29998  cvmlift2lem10  30028  cvmlift2lem12  30030  frmin  30473  wzel  30500  wsuclem  30501  nofulllem5  30588  btwndiff  30787  trisegint  30788  cgrxfr  30815  lineext  30836  segcon2  30865  brsegle2  30869  seglecgr12im  30870  segletr  30874  broutsideof3  30886  opnrebl2  30970  nn0prpw  30972  fin2so  31925  poimirlem27  31960  poimirlem30  31963  poimirlem31  31964  poimir  31966  mblfinlem1  31970  mblfinlem2  31971  mblfinlem3  31972  mblfinlem4  31973  itg2addnclem  31986  ftc1cnnc  32009  ftc1anclem5  32014  ftc1anclem6  32015  sdclem1  32065  geomcau  32081  equivtotbnd  32103  bndss  32111  ismtybndlem  32131  heibor1lem  32134  rrncmslem  32157  prtlem15  32441  lsateln0  32555  lsat0cv  32593  eqlkr3  32661  lkrshp  32665  lshpset2N  32679  hlhgt2  32948  hlrelat2  32962  atle  32995  athgt  33015  2dim  33029  1cvratex  33032  ps-2  33037  dalem20  33252  lhpexle1lem  33566  lhpexle1  33567  lhpexle2lem  33568  lhpmcvr5N  33586  lhpmcvr6N  33587  cdleme25a  33914  cdleme29ex  33935  cdlemfnid  34125  cdlemg33b0  34262  cdlemg33a  34267  cdlemg35  34274  cdleml3N  34539  dihlsscpre  34796  dih1dimb2  34803  dihatexv  34900  dvh3dim2  35010  dochkr1  35040  dochkr1OLDN  35041  lcfl8  35064  lcfl8b  35066  lcfrlem5  35108  lcfrlem6  35109  mapdrvallem2  35207  mapdh9a  35352  mapdh9aOLDN  35353  hdmaprnlem3eN  35423  hdmaprnlem16N  35427  fphpdo  35654  rencldnfilem  35657  irrapxlem2  35661  cvgdvgrat  36656  expgrowth  36678  projf1o  37468  ssfiunibd  37521  supxrgere  37550  supxrgelem  37554  suplesup  37556  infrpge  37568  qinioo  37631  climinf  37678  climinfOLD  37679  mullimc  37690  islptre  37693  limccog  37694  mullimcf  37697  limcrecl  37703  sumnnodd  37704  neglimc  37722  0ellimcdiv  37724  limclner  37726  cncfioobd  37769  stoweidlem7  37861  stoweidlem27  37881  stoweidlem39  37894  stoweidlem48  37903  stoweidlem49  37904  stoweidlem60  37915  stoweidlem61  37916  stoweid  37919  dirkercncflem2  37960  fourierdlem20  37983  fourierdlem39  38003  fourierdlem41  38005  fourierdlem48  38012  fourierdlem49  38013  fourierdlem50  38014  fourierdlem64  38028  fourierdlem73  38037  fourierdlem74  38038  fourierdlem75  38039  fourierdlem87  38051  fourierdlem103  38067  fourierdlem104  38068  qndenserrnopnlem  38160  sge0ltfirp  38236  sge0gerpmpt  38238  sge0ltfirpmpt2  38262  sge0isum  38263  sge0pnffigtmpt  38276  sge0pnffsumgt  38278  sge0gtfsumgt  38279  sge0uzfsumgt  38280  nnfoctbdjlem  38287  omeiunltfirp  38334  carageniuncllem2  38337  hoicvr  38364  volicorescl  38369  hoidmv1le  38410  hoidmvlelem3  38413  hoiqssbllem3  38440  hspmbllem2  38443  bgoldbwt  38872  bgoldbst  38873  sgoldbalt  38876  bgoldbtbndlem4  38897  bgoldbtbnd  38898  proththd  38908  zrninitoringc  40060  ply1mulgsumlem3  40167  ply1mulgsumlem4  40168  islindeps2  40263  isldepslvec2  40265
  Copyright terms: Public domain W3C validator