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

Theorem reximdva 2818
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 2816 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 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  reximddv  2819  wereu2  4704  dffo4  5847  nnaordex  7065  frfi  7545  fisupg  7548  marypha1  7672  wemapsolem  7752  unwdomg  7787  noinfepOLD  7854  rankr1ai  7993  cofsmo  8426  cfcoflem  8429  inar1  8929  nqerf  9086  prlem936  9203  dedekind  9520  fimaxre  10264  arch  10563  bndndx  10565  zmin  10936  qbtwnxr  11157  qsqueeze  11158  qextltlem  11159  xrsupsslem  11256  xrinfmsslem  11257  xrub  11261  supxrunb1  11269  expnlbnd2  11978  r19.29uz  12821  cau3lem  12825  rlim2lt  12958  rlimclim  13007  2clim  13033  o1co  13047  climcn1  13052  climcn2  13053  rlimo1  13077  climsqz  13101  climsqz2  13102  rlimsqzlem  13109  lo1le  13112  climsup  13130  climcau  13131  caucvgrlem  13133  caucvgrlem2  13135  iseralt  13145  cvgcmp  13261  cvgcmpce  13263  supcvg  13300  rpnnen2  13490  bezoutlem1  13704  exprmfct  13778  isprm5  13780  pclem  13887  pc2dvds  13927  pcprmpw  13931  unbenlem  13951  infpnlem2  13954  infpn2  13956  prmunb  13957  vdwlem2  14025  ramub1lem2  14070  drsdirfi  15090  ipodrsima  15317  grpinveu  15551  psgneu  15991  odbezout  16038  sylow2blem3  16100  sylow2  16104  gexex  16314  irredrmul  16732  lsmelval2  17087  lbsextlem2  17161  znunit  17837  neiptopnei  18577  neitr  18625  cnpnei  18709  haust1  18797  nrmsep  18802  isnrm3  18804  regsep2  18821  isreg2  18822  tgcmp  18845  hauscmplem  18850  hauscmp  18851  bwth  18854  1stcfb  18890  1stcelcls  18906  lly1stc  18941  txcmplem1  19055  txlm  19062  xkococnlem  19073  filuni  19299  filufint  19334  ufilen  19344  fclscf  19439  cnextcn  19480  ustex2sym  19632  ustex3sym  19633  utopreg  19668  isucn2  19695  ucnima  19697  ucncn  19701  neipcfilu  19712  metequiv2  19926  met1stc  19937  metrest  19940  xrsmopn  20230  mulc1cncf  20322  cncfco  20324  cnheibor  20368  bndth  20371  lmmcvg  20613  cfil3i  20621  iscau4  20631  cmetcaulem  20640  iscmet3lem1  20643  caussi  20649  equivcfil  20651  equivcau  20652  caubl  20659  lmcau  20664  minveclem3b  20756  ovolgelb  20804  ovollb2lem  20812  ovolctb  20814  ovolicc2lem4  20844  ioombl1lem4  20883  dyadmax  20919  volsup2  20926  ismbf3d  20973  itg2monolem1  21069  c1liplem1  21309  c1lip1  21310  dvivthlem1  21321  lhop1  21327  ftc1a  21350  ftc1lem6  21354  ply1divex  21492  elply2  21548  dgrlem  21581  aacjcl  21677  aalioulem2  21683  aalioulem3  21684  aalioulem4  21685  ulmcaulem  21743  ulmcau  21744  ulmss  21746  ulmdvlem3  21751  mtest  21753  itgulm  21757  reeff1o  21796  efif1olem4  21885  rlimcnp  22243  xrlimcnp  22246  ftalem3  22296  fta  22301  muval1  22355  dvdssqf  22360  mumullem1  22401  pntlem3  22742  ostth  22772  tgtrisegint  22833  tgbtwndiff  22840  tgcgrxfr  22850  lnext  22874  legov2  22892  legtrd  22895  axpasch  23009  grpoidinvlem3  23515  grpoideu  23518  grpoinveu  23531  isgrp2d  23544  rngo2  23697  ubthlem1  24093  minvecolem5  24104  htthlem  24141  pjhthlem2  24617  chscllem2  24863  nmopun  25240  lnconi  25259  rnbra  25333  sumdmdii  25641  cdj3lem2b  25663  xrofsup  25877  isarchi3  26027  isarchiofld  26137  lmxrge0  26235  lmdvg  26236  esumlub  26364  esumfsup  26372  esumcvg  26388  eulerpartlemgvv  26606  lgamucov  26871  cvmliftmolem2  27018  cvmliftlem15  27034  cvmlift2lem10  27048  cvmlift2lem12  27050  frmin  27549  wzel  27607  wsuclem  27608  nofulllem5  27693  btwndiff  27904  trisegint  27905  cgrxfr  27932  lineext  27953  segcon2  27982  brsegle2  27986  seglecgr12im  27987  segletr  27991  broutsideof3  28003  fin2so  28257  mblfinlem1  28269  mblfinlem2  28270  mblfinlem3  28271  mblfinlem4  28272  itg2addnclem  28284  ftc1cnnc  28307  ftc1anclem5  28312  ftc1anclem6  28313  opnrebl2  28357  nn0prpw  28359  locfincmp  28417  sdclem1  28480  geomcau  28496  equivtotbnd  28518  bndss  28526  ismtybndlem  28546  heibor1lem  28549  rrncmslem  28572  prtlem15  28862  nacsfix  28890  fphpdo  28998  rencldnfilem  29001  irrapxlem2  29006  unxpwdom3  29290  expgrowth  29451  climinf  29622  stoweidlem7  29645  stoweidlem27  29665  stoweidlem39  29677  stoweidlem48  29686  stoweidlem49  29687  stoweidlem60  29698  stoweidlem61  29699  stoweid  29701  wwlknredwwlkn0  30202  2pthfrgrarn2  30445  frgrawopreglem5  30484  usgreg2spot  30503  islindeps2  30723  isldepslvec2  30725  lsateln0  32210  lsat0cv  32248  eqlkr3  32316  lkrshp  32320  lshpset2N  32334  hlhgt2  32603  hlrelat2  32617  atle  32650  athgt  32670  2dim  32684  1cvratex  32687  ps-2  32692  dalem20  32907  lhpexle1lem  33221  lhpexle1  33222  lhpexle2lem  33223  lhpmcvr5N  33241  lhpmcvr6N  33242  cdleme25a  33567  cdleme29ex  33588  cdlemfnid  33778  cdlemg33b0  33915  cdlemg33a  33920  cdlemg35  33927  cdleml3N  34192  dihlsscpre  34449  dih1dimb2  34456  dihatexv  34553  dvh3dim2  34663  dochkr1  34693  dochkr1OLDN  34694  lcfl8  34717  lcfl8b  34719  lcfrlem5  34761  lcfrlem6  34762  mapdrvallem2  34860  mapdh9a  35005  mapdh9aOLDN  35006  hdmaprnlem3eN  35076  hdmaprnlem16N  35080
  Copyright terms: Public domain W3C validator