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

Theorem reximdva 2918
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 2915 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 1804   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798  df-rex 2799
This theorem is referenced by:  reximddv  2919  reximddv2  2920  wereu2  4866  dffo4  6032  nnaordex  7289  frfi  7767  fisupg  7770  marypha1  7896  wemapsolem  7978  unwdomg  8013  noinfepOLD  8080  rankr1ai  8219  cofsmo  8652  cfcoflem  8655  inar1  9156  nqerf  9311  prlem936  9428  fimaxre  10497  arch  10799  bndndx  10801  suprfinzcl  10984  zmin  11188  qbtwnxr  11409  qsqueeze  11410  qextltlem  11411  xrsupsslem  11508  xrinfmsslem  11509  xrub  11513  supxrunb1  11521  ssnn0fi  12075  fsuppmapnn0fiub0  12080  fsuppmapnn0fz  12083  expnlbnd2  12278  r19.29uz  13164  cau3lem  13168  rlim2lt  13301  rlimclim  13350  2clim  13376  o1co  13390  climcn1  13395  climcn2  13396  rlimo1  13420  climsqz  13444  climsqz2  13445  rlimsqzlem  13452  lo1le  13455  climsup  13473  climcau  13474  caucvgrlem2  13478  iseralt  13488  cvgcmp  13611  cvgcmpce  13613  supcvg  13648  rpnnen2  13940  bezoutlem1  14157  exprmfct  14232  pclem  14343  pc2dvds  14383  pcprmpw  14387  unbenlem  14407  infpnlem2  14410  infpn2  14412  prmunb  14413  vdwlem2  14481  ramub1lem2  14526  ipodrsima  15773  grpinveu  16062  psgneu  16509  odbezout  16558  sylow2blem3  16620  nn0gsumfz  16990  irredrmul  17334  lsmelval2  17709  lbsextlem2  17783  mptcoe1fsupp  18233  znunit  18579  scmate  18989  scmatscm  18992  scmatfo  19009  mat1scmat  19018  pmatcoe1fsupp  19179  pmatcollpwfi  19260  pmatcollpw3fi  19263  mptcoe1matfsupp  19280  pm2mp  19303  chmaidscmat  19326  cpmadugsum  19356  cpmadumatpoly  19361  chcoeffeq  19364  cayhamlem3  19365  cayhamlem4  19366  neiptopnei  19610  neitr  19658  cnpnei  19742  haust1  19830  isnrm3  19837  isreg2  19855  tgcmp  19878  hauscmplem  19883  hauscmp  19884  bwth  19887  1stcfb  19923  1stcelcls  19939  lly1stc  19974  txcmplem1  20119  txlm  20126  xkococnlem  20137  filuni  20363  filufint  20398  ufilen  20408  fclscf  20503  cnextcn  20544  ustex2sym  20696  ustex3sym  20697  utopreg  20732  isucn2  20759  ucnima  20761  ucncn  20765  neipcfilu  20776  metequiv2  20990  metrest  21004  xrsmopn  21294  mulc1cncf  21386  cncfco  21388  bndth  21435  lmmcvg  21677  cfil3i  21685  iscau4  21695  cmetcaulem  21704  iscmet3lem1  21707  caussi  21713  equivcfil  21715  equivcau  21716  caubl  21723  minveclem3b  21820  ovolgelb  21868  ovollb2lem  21876  ovolctb  21878  ovolicc2lem4  21908  ioombl1lem4  21948  dyadmax  21984  volsup2  21991  itg2monolem1  22134  c1liplem1  22374  c1lip1  22375  dvivthlem1  22386  lhop1  22392  ftc1a  22415  ftc1lem6  22419  ply1divex  22514  elply2  22570  dgrlem  22603  aacjcl  22699  aalioulem2  22705  aalioulem3  22706  aalioulem4  22707  ulmcaulem  22765  ulmcau  22766  ulmss  22768  mtest  22775  itgulm  22779  reeff1o  22818  efif1olem4  22908  rlimcnp  23271  xrlimcnp  23274  ftalem3  23324  fta  23329  muval1  23383  dvdssqf  23388  mumullem1  23429  pntlem3  23770  ostth  23800  tgtrisegint  23866  tgbtwndiff  23873  tgcgrxfr  23885  lnext  23930  legov2  23949  legtrd  23952  colperpexlem3  24082  colperpex  24083  hpgerlem  24110  hpgtr  24113  axpasch  24220  wwlknredwwlkn0  24703  2pthfrgrarn2  24986  frgrawopreglem5  25024  usgreg2spot  25043  grpoidinvlem3  25184  grpoideu  25187  grpoinveu  25200  isgrp2d  25213  rngo2  25366  ubthlem1  25762  minvecolem5  25773  htthlem  25810  chscllem2  26532  nmopun  26909  lnconi  26928  rnbra  27002  sumdmdii  27310  cdj3lem2b  27332  foresf1o  27379  xrofsup  27558  isarchi3  27708  isarchiofld  27784  lmxrge0  27911  lmdvg  27912  esumlub  28045  esumfsup  28053  esumcvg  28069  eulerpartlemgvv  28292  lgamucov  28557  cvmliftmolem2  28704  cvmlift2lem10  28734  cvmlift2lem12  28736  frmin  29297  wzel  29355  wsuclem  29356  nofulllem5  29441  btwndiff  29652  trisegint  29653  cgrxfr  29680  lineext  29701  segcon2  29730  brsegle2  29734  seglecgr12im  29735  segletr  29739  broutsideof3  29751  fin2so  30015  mblfinlem1  30026  mblfinlem2  30027  mblfinlem3  30028  mblfinlem4  30029  itg2addnclem  30041  ftc1cnnc  30064  ftc1anclem5  30069  ftc1anclem6  30070  opnrebl2  30114  nn0prpw  30116  sdclem1  30211  geomcau  30227  equivtotbnd  30249  bndss  30257  ismtybndlem  30277  heibor1lem  30280  rrncmslem  30303  prtlem15  30591  fphpdo  30726  rencldnfilem  30729  irrapxlem2  30734  cvgdvgrat  31170  lcmgcdlem  31188  expgrowth  31216  ssfiunibd  31458  climinf  31520  mullimc  31530  islptre  31533  limccog  31534  mullimcf  31537  limcrecl  31543  sumnnodd  31544  neglimc  31561  0ellimcdiv  31563  limclner  31565  cncfioobd  31607  stoweidlem7  31678  stoweidlem27  31698  stoweidlem39  31710  stoweidlem48  31719  stoweidlem49  31720  stoweidlem60  31731  stoweidlem61  31732  stoweid  31734  dirkercncflem2  31775  fourierdlem20  31798  fourierdlem39  31817  fourierdlem41  31819  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem64  31842  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem87  31865  fourierdlem103  31881  fourierdlem104  31882  ply1mulgsumlem3  32723  ply1mulgsumlem4  32724  islindeps2  32819  isldepslvec2  32821  lsateln0  34460  lsat0cv  34498  eqlkr3  34566  lkrshp  34570  lshpset2N  34584  hlhgt2  34853  hlrelat2  34867  atle  34900  athgt  34920  2dim  34934  1cvratex  34937  ps-2  34942  dalem20  35157  lhpexle1lem  35471  lhpexle1  35472  lhpexle2lem  35473  lhpmcvr5N  35491  lhpmcvr6N  35492  cdleme25a  35819  cdleme29ex  35840  cdlemfnid  36030  cdlemg33b0  36167  cdlemg33a  36172  cdlemg35  36179  cdleml3N  36444  dihlsscpre  36701  dih1dimb2  36708  dihatexv  36805  dvh3dim2  36915  dochkr1  36945  dochkr1OLDN  36946  lcfl8  36969  lcfl8b  36971  lcfrlem5  37013  lcfrlem6  37014  mapdrvallem2  37112  mapdh9a  37257  mapdh9aOLDN  37258  hdmaprnlem3eN  37328  hdmaprnlem16N  37332
  Copyright terms: Public domain W3C validator