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

Theorem reximdva 2849
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 2847 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 1756   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2741  df-rex 2742
This theorem is referenced by:  reximddv  2850  wereu2  4738  dffo4  5880  nnaordex  7098  frfi  7578  fisupg  7581  marypha1  7705  wemapsolem  7785  unwdomg  7820  noinfepOLD  7887  rankr1ai  8026  cofsmo  8459  cfcoflem  8462  inar1  8963  nqerf  9120  prlem936  9237  dedekind  9554  fimaxre  10298  arch  10597  bndndx  10599  zmin  10970  qbtwnxr  11191  qsqueeze  11192  qextltlem  11193  xrsupsslem  11290  xrinfmsslem  11291  xrub  11295  supxrunb1  11303  expnlbnd2  12016  r19.29uz  12859  cau3lem  12863  rlim2lt  12996  rlimclim  13045  2clim  13071  o1co  13085  climcn1  13090  climcn2  13091  rlimo1  13115  climsqz  13139  climsqz2  13140  rlimsqzlem  13147  lo1le  13150  climsup  13168  climcau  13169  caucvgrlem  13171  caucvgrlem2  13173  iseralt  13183  cvgcmp  13300  cvgcmpce  13302  supcvg  13339  rpnnen2  13529  bezoutlem1  13743  exprmfct  13817  isprm5  13819  pclem  13926  pc2dvds  13966  pcprmpw  13970  unbenlem  13990  infpnlem2  13993  infpn2  13995  prmunb  13996  vdwlem2  14064  ramub1lem2  14109  drsdirfi  15129  ipodrsima  15356  grpinveu  15593  psgneu  16033  odbezout  16080  sylow2blem3  16142  sylow2  16146  gexex  16356  irredrmul  16821  lsmelval2  17188  lbsextlem2  17262  znunit  18018  neiptopnei  18758  neitr  18806  cnpnei  18890  haust1  18978  nrmsep  18983  isnrm3  18985  regsep2  19002  isreg2  19003  tgcmp  19026  hauscmplem  19031  hauscmp  19032  bwth  19035  1stcfb  19071  1stcelcls  19087  lly1stc  19122  txcmplem1  19236  txlm  19243  xkococnlem  19254  filuni  19480  filufint  19515  ufilen  19525  fclscf  19620  cnextcn  19661  ustex2sym  19813  ustex3sym  19814  utopreg  19849  isucn2  19876  ucnima  19878  ucncn  19882  neipcfilu  19893  metequiv2  20107  met1stc  20118  metrest  20121  xrsmopn  20411  mulc1cncf  20503  cncfco  20505  cnheibor  20549  bndth  20552  lmmcvg  20794  cfil3i  20802  iscau4  20812  cmetcaulem  20821  iscmet3lem1  20824  caussi  20830  equivcfil  20832  equivcau  20833  caubl  20840  lmcau  20845  minveclem3b  20937  ovolgelb  20985  ovollb2lem  20993  ovolctb  20995  ovolicc2lem4  21025  ioombl1lem4  21064  dyadmax  21100  volsup2  21107  ismbf3d  21154  itg2monolem1  21250  c1liplem1  21490  c1lip1  21491  dvivthlem1  21502  lhop1  21508  ftc1a  21531  ftc1lem6  21535  ply1divex  21630  elply2  21686  dgrlem  21719  aacjcl  21815  aalioulem2  21821  aalioulem3  21822  aalioulem4  21823  ulmcaulem  21881  ulmcau  21882  ulmss  21884  ulmdvlem3  21889  mtest  21891  itgulm  21895  reeff1o  21934  efif1olem4  22023  rlimcnp  22381  xrlimcnp  22384  ftalem3  22434  fta  22439  muval1  22493  dvdssqf  22498  mumullem1  22539  pntlem3  22880  ostth  22910  tgtrisegint  22974  tgbtwndiff  22981  tgcgrxfr  22992  lnext  23021  legov2  23039  legtrd  23042  axpasch  23209  grpoidinvlem3  23715  grpoideu  23718  grpoinveu  23731  isgrp2d  23744  rngo2  23897  ubthlem1  24293  minvecolem5  24304  htthlem  24341  pjhthlem2  24817  chscllem2  25063  nmopun  25440  lnconi  25459  rnbra  25533  sumdmdii  25841  cdj3lem2b  25863  xrofsup  26077  isarchi3  26226  isarchiofld  26307  lmxrge0  26404  lmdvg  26405  esumlub  26533  esumfsup  26541  esumcvg  26557  eulerpartlemgvv  26781  lgamucov  27046  cvmliftmolem2  27193  cvmliftlem15  27209  cvmlift2lem10  27223  cvmlift2lem12  27225  frmin  27725  wzel  27783  wsuclem  27784  nofulllem5  27869  btwndiff  28080  trisegint  28081  cgrxfr  28108  lineext  28129  segcon2  28158  brsegle2  28162  seglecgr12im  28163  segletr  28167  broutsideof3  28179  fin2so  28442  mblfinlem1  28454  mblfinlem2  28455  mblfinlem3  28456  mblfinlem4  28457  itg2addnclem  28469  ftc1cnnc  28492  ftc1anclem5  28497  ftc1anclem6  28498  opnrebl2  28542  nn0prpw  28544  locfincmp  28602  sdclem1  28665  geomcau  28681  equivtotbnd  28703  bndss  28711  ismtybndlem  28731  heibor1lem  28734  rrncmslem  28757  prtlem15  29046  nacsfix  29074  fphpdo  29182  rencldnfilem  29185  irrapxlem2  29190  unxpwdom3  29474  expgrowth  29635  climinf  29805  stoweidlem7  29828  stoweidlem27  29848  stoweidlem39  29860  stoweidlem48  29869  stoweidlem49  29870  stoweidlem60  29881  stoweidlem61  29882  stoweid  29884  wwlknredwwlkn0  30385  2pthfrgrarn2  30628  frgrawopreglem5  30667  usgreg2spot  30686  suprfinzcl  30774  ssnn0fi  30775  fsuppmapnn0fz  30827  fsuppmapnn0fiub0  30831  nn0gsumfz  30837  mptcoe1fsupp  30866  ply1mulgsumlem3  30879  ply1mulgsumlem4  30880  islindeps2  31014  isldepslvec2  31016  mptcoe1matfsupp  31106  pmatcoe1fsupp  31107  pmattomply1mhmlem0  31142  pmattomply1mhmlem1  31143  lsateln0  32736  lsat0cv  32774  eqlkr3  32842  lkrshp  32846  lshpset2N  32860  hlhgt2  33129  hlrelat2  33143  atle  33176  athgt  33196  2dim  33210  1cvratex  33213  ps-2  33218  dalem20  33433  lhpexle1lem  33747  lhpexle1  33748  lhpexle2lem  33749  lhpmcvr5N  33767  lhpmcvr6N  33768  cdleme25a  34093  cdleme29ex  34114  cdlemfnid  34304  cdlemg33b0  34441  cdlemg33a  34446  cdlemg35  34453  cdleml3N  34718  dihlsscpre  34975  dih1dimb2  34982  dihatexv  35079  dvh3dim2  35189  dochkr1  35219  dochkr1OLDN  35220  lcfl8  35243  lcfl8b  35245  lcfrlem5  35287  lcfrlem6  35288  mapdrvallem2  35386  mapdh9a  35531  mapdh9aOLDN  35532  hdmaprnlem3eN  35602  hdmaprnlem16N  35606
  Copyright terms: Public domain W3C validator