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

Theorem reximdva 2630
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 2628 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 2519
This theorem is referenced by:  wereu2  4362  dffo4  5610  nnaordex  6604  frfi  7070  fisupg  7073  marypha1  7155  wemapso2lem  7233  unwdomg  7266  noinfepOLD  7329  rankr1ai  7438  cofsmo  7863  cfcoflem  7866  inar1  8365  nqerf  8522  prlem936  8639  fimaxre  9669  arch  9929  bndndx  9931  zmin  10279  qbtwnxr  10493  qsqueeze  10494  qextltlem  10495  xrsupsslem  10591  xrinfmsslem  10592  xrub  10596  supxrunb1  10604  expnlbnd2  11198  r19.29uz  11799  cau3lem  11803  rlim2lt  11936  rlimclim  11985  2clim  12011  o1co  12025  climcn1  12030  climcn2  12031  rlimo1  12055  climsqz  12079  climsqz2  12080  rlimsqzlem  12087  lo1le  12090  climsup  12108  climcau  12109  caucvgrlem  12110  caucvgrlem2  12112  iseralt  12122  cvgcmp  12239  cvgcmpce  12241  supcvg  12276  rpnnen2  12466  bezoutlem1  12679  exprmfct  12751  isprm5  12753  pclem  12853  pc2dvds  12893  pcprmpw  12897  unbenlem  12917  infpnlem2  12920  infpn2  12922  prmunb  12923  vdwlem2  12991  ramub1lem2  13036  drsdirfi  14034  ipodrsima  14230  grpinveu  14478  odbezout  14833  sylow2blem3  14895  sylow2  14899  gexex  15107  irredrmul  15451  lsmelval2  15800  lbsextlem2  15874  znunit  16479  cnpnei  16955  haust1  17042  nrmsep  17047  isnrm3  17049  regsep2  17066  isreg2  17067  tgcmp  17090  hauscmplem  17095  hauscmp  17096  1stcfb  17133  1stcelcls  17149  lly1stc  17184  txcmplem1  17297  txlm  17304  xkococnlem  17315  filuni  17542  filufint  17577  ufilen  17587  fclscf  17682  metequiv2  18018  met1stc  18029  metrest  18032  xrsmopn  18280  xrge0tsms  18301  mulc1cncf  18371  cncfco  18373  cnheibor  18415  bndth  18418  lmmcvg  18649  cfil3i  18657  iscau4  18667  cmetcaulem  18676  iscmet3lem1  18679  caussi  18685  equivcfil  18687  equivcau  18688  caubl  18695  lmcau  18700  minveclem3b  18754  ovolgelb  18801  ovollb2lem  18809  ovolctb  18811  ovolicc2lem4  18841  ioombl1lem4  18880  dyadmax  18915  volsup2  18922  ismbf3d  18971  itg2monolem1  19067  c1liplem1  19305  c1lip1  19306  dvivthlem1  19317  lhop1  19323  ftc1a  19346  ftc1lem6  19350  ply1divex  19484  elply2  19540  dgrlem  19573  aacjcl  19669  aalioulem2  19675  aalioulem3  19676  aalioulem4  19677  ulmcaulem  19733  ulmcau  19734  ulmss  19736  ulmdvlem3  19741  mtest  19743  itgulm  19746  reeff1o  19785  efif1olem4  19869  rlimcnp  20222  xrlimcnp  20225  ftalem3  20274  fta  20279  muval1  20333  dvdssqf  20338  mumullem1  20379  pntlem3  20720  ostth  20750  grpoidinvlem3  20833  grpoideu  20836  grpoinveu  20849  isgrp2d  20862  rngo2  21015  ubthlem1  21409  minvecolem5  21420  htthlem  21457  pjhthlem2  21931  chscllem2  22177  nmopun  22554  lnconi  22573  rnbra  22647  sumdmdii  22955  cdj3lem2b  22977  reximddv  22988  cvmliftmolem2  23185  cvmliftlem15  23201  cvmlift2lem10  23215  cvmlift2lem12  23217  dedekind  23453  frmin  23611  axfelem18  23732  axfelem22  23736  axpasch  23944  btwndiff  24025  trisegint  24026  cgrxfr  24053  lineext  24074  segcon2  24103  brsegle2  24107  seglecgr12im  24108  segletr  24112  broutsideof3  24124  pdiveql  25535  abhp  25540  opnrebl2  25603  nn0prpw  25606  locfincmp  25671  sdclem1  25820  geomcau  25842  equivtotbnd  25869  bndss  25877  ismtybndlem  25897  heibor1lem  25900  rrncmslem  25923  prtlem15  26110  nacsfix  26154  fphpdo  26267  rencldnfilem  26270  irrapxlem2  26275  unxpwdom3  26623  psgneu  26796  expgrowth  26919  stoweidlem7  27091  stoweidlem27  27111  stoweidlem39  27123  stoweidlem48  27132  stoweidlem49  27133  stoweidlem60  27144  stoweidlem61  27145  stoweid  27147  lsateln0  28352  lsat0cv  28390  eqlkr3  28458  lkrshp  28462  lshpset2N  28476  hlhgt2  28745  hlrelat2  28759  atle  28792  athgt  28812  2dim  28826  1cvratex  28829  ps-2  28834  dalem20  29049  lhpexle1lem  29363  lhpexle1  29364  lhpexle2lem  29365  lhpmcvr5N  29383  lhpmcvr6N  29384  cdleme25a  29709  cdleme29ex  29730  cdlemfnid  29920  cdlemg33b0  30057  cdlemg33a  30062  cdlemg35  30069  cdleml3N  30334  dihlsscpre  30591  dih1dimb2  30598  dihatexv  30695  dvh3dim2  30805  dochkr1  30835  dochkr1OLDN  30836  lcfl8  30859  lcfl8b  30861  lcfrlem5  30903  lcfrlem6  30904  mapdrvallem2  31002  mapdh9a  31147  mapdh9aOLDN  31148  hdmaprnlem3eN  31218  hdmaprnlem16N  31222
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 2523  df-rex 2524
  Copyright terms: Public domain W3C validator