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

Theorem reximdva 2656
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 425 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2654 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1685   E.wrex 2545
This theorem is referenced by:  wereu2  4389  dffo4  5637  nnaordex  6631  frfi  7097  fisupg  7100  marypha1  7182  wemapso2lem  7260  unwdomg  7293  noinfepOLD  7356  rankr1ai  7465  cofsmo  7890  cfcoflem  7893  inar1  8392  nqerf  8549  prlem936  8666  fimaxre  9696  arch  9957  bndndx  9959  zmin  10307  qbtwnxr  10521  qsqueeze  10522  qextltlem  10523  xrsupsslem  10619  xrinfmsslem  10620  xrub  10624  supxrunb1  10632  expnlbnd2  11226  r19.29uz  11828  cau3lem  11832  rlim2lt  11965  rlimclim  12014  2clim  12040  o1co  12054  climcn1  12059  climcn2  12060  rlimo1  12084  climsqz  12108  climsqz2  12109  rlimsqzlem  12116  lo1le  12119  climsup  12137  climcau  12138  caucvgrlem  12139  caucvgrlem2  12141  iseralt  12151  cvgcmp  12268  cvgcmpce  12270  supcvg  12308  rpnnen2  12498  bezoutlem1  12711  exprmfct  12783  isprm5  12785  pclem  12885  pc2dvds  12925  pcprmpw  12929  unbenlem  12949  infpnlem2  12952  infpn2  12954  prmunb  12955  vdwlem2  13023  ramub1lem2  13068  drsdirfi  14066  ipodrsima  14262  grpinveu  14510  odbezout  14865  sylow2blem3  14927  sylow2  14931  gexex  15139  irredrmul  15483  lsmelval2  15832  lbsextlem2  15906  znunit  16511  cnpnei  16987  haust1  17074  nrmsep  17079  isnrm3  17081  regsep2  17098  isreg2  17099  tgcmp  17122  hauscmplem  17127  hauscmp  17128  1stcfb  17165  1stcelcls  17181  lly1stc  17216  txcmplem1  17329  txlm  17336  xkococnlem  17347  filuni  17574  filufint  17609  ufilen  17619  fclscf  17714  metequiv2  18050  met1stc  18061  metrest  18064  xrsmopn  18312  xrge0tsms  18333  mulc1cncf  18403  cncfco  18405  cnheibor  18447  bndth  18450  lmmcvg  18681  cfil3i  18689  iscau4  18699  cmetcaulem  18708  iscmet3lem1  18711  caussi  18717  equivcfil  18719  equivcau  18720  caubl  18727  lmcau  18732  minveclem3b  18786  ovolgelb  18833  ovollb2lem  18841  ovolctb  18843  ovolicc2lem4  18873  ioombl1lem4  18912  dyadmax  18947  volsup2  18954  ismbf3d  19003  itg2monolem1  19099  c1liplem1  19337  c1lip1  19338  dvivthlem1  19349  lhop1  19355  ftc1a  19378  ftc1lem6  19382  ply1divex  19516  elply2  19572  dgrlem  19605  aacjcl  19701  aalioulem2  19707  aalioulem3  19708  aalioulem4  19709  ulmcaulem  19765  ulmcau  19766  ulmss  19768  ulmdvlem3  19773  mtest  19775  itgulm  19778  reeff1o  19817  efif1olem4  19901  rlimcnp  20254  xrlimcnp  20257  ftalem3  20306  fta  20311  muval1  20365  dvdssqf  20370  mumullem1  20411  pntlem3  20752  ostth  20782  grpoidinvlem3  20865  grpoideu  20868  grpoinveu  20881  isgrp2d  20894  rngo2  21047  ubthlem1  21441  minvecolem5  21452  htthlem  21489  pjhthlem2  21963  chscllem2  22209  nmopun  22586  lnconi  22605  rnbra  22679  sumdmdii  22987  cdj3lem2b  23009  reximddv  23020  cvmliftmolem2  23217  cvmliftlem15  23233  cvmlift2lem10  23247  cvmlift2lem12  23249  dedekind  23485  frmin  23643  axfelem18  23764  axfelem22  23768  axpasch  23976  btwndiff  24057  trisegint  24058  cgrxfr  24085  lineext  24106  segcon2  24135  brsegle2  24139  seglecgr12im  24140  segletr  24144  broutsideof3  24156  pdiveql  25567  abhp  25572  opnrebl2  25635  nn0prpw  25638  locfincmp  25703  sdclem1  25852  geomcau  25874  equivtotbnd  25901  bndss  25909  ismtybndlem  25929  heibor1lem  25932  rrncmslem  25955  prtlem15  26142  nacsfix  26186  fphpdo  26299  rencldnfilem  26302  irrapxlem2  26307  unxpwdom3  26655  psgneu  26828  expgrowth  26951  climinf  27131  stoweidlem7  27155  stoweidlem27  27175  stoweidlem39  27187  stoweidlem48  27196  stoweidlem49  27197  stoweidlem60  27208  stoweidlem61  27209  stoweid  27211  lsateln0  28452  lsat0cv  28490  eqlkr3  28558  lkrshp  28562  lshpset2N  28576  hlhgt2  28845  hlrelat2  28859  atle  28892  athgt  28912  2dim  28926  1cvratex  28929  ps-2  28934  dalem20  29149  lhpexle1lem  29463  lhpexle1  29464  lhpexle2lem  29465  lhpmcvr5N  29483  lhpmcvr6N  29484  cdleme25a  29809  cdleme29ex  29830  cdlemfnid  30020  cdlemg33b0  30157  cdlemg33a  30162  cdlemg35  30169  cdleml3N  30434  dihlsscpre  30691  dih1dimb2  30698  dihatexv  30795  dvh3dim2  30905  dochkr1  30935  dochkr1OLDN  30936  lcfl8  30959  lcfl8b  30961  lcfrlem5  31003  lcfrlem6  31004  mapdrvallem2  31102  mapdh9a  31247  mapdh9aOLDN  31248  hdmaprnlem3eN  31318  hdmaprnlem16N  31322
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator