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

Theorem reximdva 2898
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 435 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2895 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1867   E.wrex 2774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2778  df-rex 2779
This theorem is referenced by:  reximddv  2899  reximddv2  2900  wereu2  4843  dffo4  6045  nnaordex  7339  frfi  7814  fisupg  7817  marypha1  7946  fiinfg  8013  wemapsolem  8063  unwdomg  8097  rankr1ai  8266  cofsmo  8695  cfcoflem  8698  inar1  9196  nqerf  9351  prlem936  9468  fimaxre  10547  arch  10862  bndndx  10864  suprfinzcl  11046  zmin  11256  qbtwnxr  11489  qsqueeze  11490  qextltlem  11491  xrsupsslem  11588  xrinfmsslem  11589  xrub  11593  supxrunb1  11601  ssnn0fi  12190  fsuppmapnn0fiub0  12198  fsuppmapnn0fz  12201  expnlbnd2  12396  r19.29uz  13392  cau3lem  13396  rlim2lt  13539  rlimclim  13588  2clim  13614  o1co  13628  climcn1  13633  climcn2  13634  rlimo1  13658  climsqz  13682  climsqz2  13683  rlimsqzlem  13690  lo1le  13693  climsup  13711  climcau  13712  caucvgrlem2  13718  iseralt  13729  cvgcmp  13854  cvgcmpce  13856  supcvg  13892  rpnnen2  14256  bezoutlem1  14481  lcmgcdlem  14549  exprmfct  14626  prmdvdsfz  14627  pclem  14766  pc2dvds  14806  pcprmpw  14810  unbenlem  14830  infpnlem2  14833  infpn2  14835  prmunb  14836  vdwlem2  14910  ramub1lem2  14963  prmdvdsprmop  14979  prmdvdsprmorpOLD  14994  prmgaplem7  15005  ipodrsima  16389  grpinveu  16678  psgneu  17125  odbezout  17187  sylow2blem3  17252  nn0gsumfz  17591  irredrmul  17913  lsmelval2  18286  lbsextlem2  18360  mptcoe1fsupp  18786  znunit  19111  scmate  19512  scmatscm  19515  scmatfo  19532  mat1scmat  19541  pmatcoe1fsupp  19702  pmatcollpwfi  19783  pmatcollpw3fi  19786  mptcoe1matfsupp  19803  pm2mp  19826  chmaidscmat  19849  cpmadugsum  19879  cpmadumatpoly  19884  chcoeffeq  19887  cayhamlem3  19888  cayhamlem4  19889  neiptopnei  20125  neitr  20173  cnpnei  20257  haust1  20345  isnrm3  20352  isreg2  20370  tgcmp  20393  hauscmplem  20398  hauscmp  20399  bwth  20402  1stcfb  20437  1stcelcls  20453  lly1stc  20488  txcmplem1  20633  txlm  20640  xkococnlem  20651  filuni  20877  filufint  20912  ufilen  20922  fclscf  21017  cnextcn  21059  ustex2sym  21208  ustex3sym  21209  utopreg  21244  isucn2  21271  ucnima  21273  ucncn  21277  neipcfilu  21288  metequiv2  21502  metrest  21516  xrsmopn  21807  mulc1cncf  21914  cncfco  21916  bndth  21963  lmmcvg  22208  cfil3i  22216  iscau4  22226  cmetcaulem  22235  iscmet3lem1  22238  caussi  22244  equivcfil  22246  equivcau  22247  caubl  22254  minveclem3b  22347  minveclem3bOLD  22359  ovolgelb  22410  ovollb2lem  22418  ovolctb  22420  ovolicc2lem4OLD  22450  ovolicc2lem4  22451  ioombl1lem4  22491  dyadmax  22533  volsup2  22540  itg2monolem1  22685  c1liplem1  22925  c1lip1  22926  dvivthlem1  22937  lhop1  22943  ftc1a  22966  ftc1lem6  22970  ply1divex  23064  elply2  23127  dgrlem  23160  aacjcl  23260  aalioulem2  23266  aalioulem3  23267  aalioulem4  23268  ulmcaulem  23326  ulmcau  23327  ulmss  23329  mtest  23336  itgulm  23340  reeff1o  23379  efif1olem4  23471  rlimcnp  23868  xrlimcnp  23871  lgamucov  23940  ftalem3  23976  fta  23983  muval1  24037  dvdssqf  24042  mumullem1  24083  pntlem3  24424  ostth  24454  tgtrisegint  24520  tgbtwndiff  24527  tgcgrxfr  24540  lnext  24589  legov2  24608  legtrd  24611  hlcgrex  24638  colperpexlem3  24751  colperpex  24752  hlpasch  24775  hpgerlem  24784  hpgtr  24787  dfcgra2  24848  acopy  24851  inagswap  24857  inaghl  24858  cgrg3col4  24861  axpasch  24948  wwlknredwwlkn0  25431  2pthfrgrarn2  25714  frgrawopreglem5  25752  usgreg2spot  25771  grpoidinvlem3  25910  grpoideu  25913  grpoinveu  25926  isgrp2d  25939  rngo2  26092  ubthlem1  26488  minvecolem5  26499  minvecolem5OLD  26509  htthlem  26546  chscllem2  27267  nmopun  27643  lnconi  27662  rnbra  27736  sumdmdii  28044  cdj3lem2b  28066  foresf1o  28116  acunirnmpt  28242  xrofsup  28338  isarchi3  28492  isarchiofld  28569  lmxrge0  28747  lmdvg  28748  esumlub  28870  esumfsup  28880  esumcvg  28896  eulerpartlemgvv  29198  cvmliftmolem2  29994  cvmlift2lem10  30024  cvmlift2lem12  30026  frmin  30468  wzel  30495  wsuclem  30496  nofulllem5  30581  btwndiff  30780  trisegint  30781  cgrxfr  30808  lineext  30829  segcon2  30858  brsegle2  30862  seglecgr12im  30863  segletr  30867  broutsideof3  30879  opnrebl2  30963  nn0prpw  30965  fin2so  31840  poimirlem27  31875  poimirlem30  31878  poimirlem31  31879  poimir  31881  mblfinlem1  31885  mblfinlem2  31886  mblfinlem3  31887  mblfinlem4  31888  itg2addnclem  31901  ftc1cnnc  31924  ftc1anclem5  31929  ftc1anclem6  31930  sdclem1  31980  geomcau  31996  equivtotbnd  32018  bndss  32026  ismtybndlem  32046  heibor1lem  32049  rrncmslem  32072  prtlem15  32359  lsateln0  32474  lsat0cv  32512  eqlkr3  32580  lkrshp  32584  lshpset2N  32598  hlhgt2  32867  hlrelat2  32881  atle  32914  athgt  32934  2dim  32948  1cvratex  32951  ps-2  32956  dalem20  33171  lhpexle1lem  33485  lhpexle1  33486  lhpexle2lem  33487  lhpmcvr5N  33505  lhpmcvr6N  33506  cdleme25a  33833  cdleme29ex  33854  cdlemfnid  34044  cdlemg33b0  34181  cdlemg33a  34186  cdlemg35  34193  cdleml3N  34458  dihlsscpre  34715  dih1dimb2  34722  dihatexv  34819  dvh3dim2  34929  dochkr1  34959  dochkr1OLDN  34960  lcfl8  34983  lcfl8b  34985  lcfrlem5  35027  lcfrlem6  35028  mapdrvallem2  35126  mapdh9a  35271  mapdh9aOLDN  35272  hdmaprnlem3eN  35342  hdmaprnlem16N  35346  fphpdo  35573  rencldnfilem  35576  irrapxlem2  35581  cvgdvgrat  36514  expgrowth  36536  ssfiunibd  37351  supxrgere  37380  supxrgelem  37384  suplesup  37386  climinf  37471  climinfOLD  37472  mullimc  37483  islptre  37486  limccog  37487  mullimcf  37490  limcrecl  37496  sumnnodd  37497  neglimc  37515  0ellimcdiv  37517  limclner  37519  cncfioobd  37562  stoweidlem7  37654  stoweidlem27  37674  stoweidlem39  37687  stoweidlem48  37696  stoweidlem49  37697  stoweidlem60  37708  stoweidlem61  37709  stoweid  37712  dirkercncflem2  37753  fourierdlem20  37776  fourierdlem39  37796  fourierdlem41  37798  fourierdlem48  37805  fourierdlem49  37806  fourierdlem50  37807  fourierdlem64  37821  fourierdlem73  37830  fourierdlem74  37831  fourierdlem75  37832  fourierdlem87  37844  fourierdlem103  37860  fourierdlem104  37861  sge0ltfirp  37997  sge0gerpmpt  37999  nnfoctbdjlem  38023  omeiunltfirp  38070  carageniuncllem2  38073  bgoldbwt  38498  bgoldbst  38499  sgoldbalt  38502  bgoldbtbndlem4  38523  bgoldbtbnd  38524  proththd  38534  zrninitoringc  39135  ply1mulgsumlem3  39244  ply1mulgsumlem4  39245  islindeps2  39340  isldepslvec2  39342
  Copyright terms: Public domain W3C validator