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

Theorem reximdva 2617
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 2615 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 1621   E.wrex 2510
This theorem is referenced by:  wereu2  4283  dffo4  5528  nnaordex  6522  frfi  6987  fisupg  6990  marypha1  7071  wemapso2lem  7149  unwdomg  7182  noinfepOLD  7245  rankr1ai  7354  cofsmo  7779  cfcoflem  7782  inar1  8277  nqerf  8434  prlem936  8551  fimaxre  9581  arch  9841  bndndx  9843  zmin  10191  qbtwnxr  10405  qsqueeze  10406  qextltlem  10407  xrsupsslem  10503  xrinfmsslem  10504  xrub  10508  supxrunb1  10516  expnlbnd2  11110  r19.29uz  11711  cau3lem  11715  rlim2lt  11848  rlimclim  11897  2clim  11923  o1co  11937  climcn1  11942  climcn2  11943  rlimo1  11967  climsqz  11991  climsqz2  11992  rlimsqzlem  11999  lo1le  12002  climsup  12020  climcau  12021  caucvgrlem  12022  caucvgrlem2  12024  iseralt  12034  cvgcmp  12151  cvgcmpce  12153  supcvg  12188  rpnnen2  12378  bezoutlem1  12591  exprmfct  12663  isprm5  12665  pclem  12765  pc2dvds  12805  pcprmpw  12809  unbenlem  12829  infpnlem2  12832  infpn2  12834  prmunb  12835  vdwlem2  12903  ramub1lem2  12948  drsdirfi  13916  ipodrsima  14112  grpinveu  14351  odbezout  14706  sylow2blem3  14768  sylow2  14772  gexex  14980  irredrmul  15324  lsmelval2  15673  lbsextlem2  15744  znunit  16349  cnpnei  16825  haust1  16912  nrmsep  16917  isnrm3  16919  regsep2  16936  isreg2  16937  tgcmp  16960  hauscmplem  16965  hauscmp  16966  1stcfb  17003  1stcelcls  17019  lly1stc  17054  txcmplem1  17167  txlm  17174  xkococnlem  17185  filuni  17412  filufint  17447  ufilen  17457  fclscf  17552  metequiv2  17888  met1stc  17899  metrest  17902  xrsmopn  18150  xrge0tsms  18171  mulc1cncf  18241  cncfco  18243  cnheibor  18285  bndth  18288  lmmcvg  18519  cfil3i  18527  iscau4  18537  cmetcaulem  18546  iscmet3lem1  18549  caussi  18555  equivcfil  18557  equivcau  18558  caubl  18565  lmcau  18570  minveclem3b  18624  ovolgelb  18671  ovollb2lem  18679  ovolctb  18681  ovolicc2lem4  18711  ioombl1lem4  18750  dyadmax  18785  volsup2  18792  ismbf3d  18841  itg2monolem1  18937  c1liplem1  19175  c1lip1  19176  dvivthlem1  19187  lhop1  19193  ftc1a  19216  ftc1lem6  19220  ply1divex  19354  elply2  19410  dgrlem  19443  aacjcl  19539  aalioulem2  19545  aalioulem3  19546  aalioulem4  19547  ulmcaulem  19603  ulmcau  19604  ulmss  19606  ulmdvlem3  19611  mtest  19613  itgulm  19616  reeff1o  19655  efif1olem4  19739  rlimcnp  20092  xrlimcnp  20095  ftalem3  20144  fta  20149  muval1  20203  dvdssqf  20208  mumullem1  20249  pntlem3  20590  ostth  20620  grpoidinvlem3  20703  grpoideu  20706  grpoinveu  20719  isgrp2d  20732  rngo2  20885  ubthlem1  21279  minvecolem5  21290  htthlem  21327  pjhthlem2  21801  chscllem2  22065  nmopun  22424  lnconi  22443  rnbra  22517  sumdmdii  22825  cdj3lem2b  22847  cvmliftmolem2  22984  cvmliftlem15  23000  cvmlift2lem10  23014  cvmlift2lem12  23016  dedekind  23252  frmin  23410  axfelem18  23531  axfelem22  23535  axpasch  23743  btwndiff  23824  trisegint  23825  cgrxfr  23852  lineext  23873  segcon2  23902  brsegle2  23906  seglecgr12im  23907  segletr  23911  broutsideof3  23923  pdiveql  25334  abhp  25339  opnrebl2  25402  nn0prpw  25405  locfincmp  25470  sdclem1  25619  geomcau  25641  equivtotbnd  25668  bndss  25676  ismtybndlem  25696  heibor1lem  25699  rrncmslem  25722  prtlem15  25909  nacsfix  25953  fphpdo  26066  rencldnfilem  26069  irrapxlem2  26074  unxpwdom3  26422  psgneu  26595  expgrowth  26718  lsateln0  27986  lsat0cv  28024  eqlkr3  28092  lkrshp  28096  lshpset2N  28110  hlhgt2  28379  hlrelat2  28393  atle  28426  athgt  28446  2dim  28460  1cvratex  28463  ps-2  28468  dalem20  28683  lhpexle1lem  28997  lhpexle1  28998  lhpexle2lem  28999  lhpmcvr5N  29017  lhpmcvr6N  29018  cdleme25a  29343  cdleme29ex  29364  cdlemfnid  29554  cdlemg33b0  29691  cdlemg33a  29696  cdlemg35  29703  cdleml3N  29968  dihlsscpre  30225  dih1dimb2  30232  dihatexv  30329  dvh3dim2  30439  dochkr1  30469  dochkr1OLDN  30470  lcfl8  30493  lcfl8b  30495  lcfrlem5  30537  lcfrlem6  30538  mapdrvallem2  30636  mapdh9a  30781  mapdh9aOLDN  30782  hdmaprnlem3eN  30852  hdmaprnlem16N  30856
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator