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

Theorem reximdva 2655
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 423 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2653 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  wereu2  4390  dffo4  5676  nnaordex  6636  frfi  7102  fisupg  7105  marypha1  7187  wemapso2lem  7265  unwdomg  7298  noinfepOLD  7361  rankr1ai  7470  cofsmo  7895  cfcoflem  7898  inar1  8397  nqerf  8554  prlem936  8671  fimaxre  9701  arch  9962  bndndx  9964  zmin  10312  qbtwnxr  10527  qsqueeze  10528  qextltlem  10529  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrunb1  10638  expnlbnd2  11232  r19.29uz  11834  cau3lem  11838  rlim2lt  11971  rlimclim  12020  2clim  12046  o1co  12060  climcn1  12065  climcn2  12066  rlimo1  12090  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  lo1le  12125  climsup  12143  climcau  12144  caucvgrlem  12145  caucvgrlem2  12147  iseralt  12157  cvgcmp  12274  cvgcmpce  12276  supcvg  12314  rpnnen2  12504  bezoutlem1  12717  exprmfct  12789  isprm5  12791  pclem  12891  pc2dvds  12931  pcprmpw  12935  unbenlem  12955  infpnlem2  12958  infpn2  12960  prmunb  12961  vdwlem2  13029  ramub1lem2  13074  drsdirfi  14072  ipodrsima  14268  grpinveu  14516  odbezout  14871  sylow2blem3  14933  sylow2  14937  gexex  15145  irredrmul  15489  lsmelval2  15838  lbsextlem2  15912  znunit  16517  cnpnei  16993  haust1  17080  nrmsep  17085  isnrm3  17087  regsep2  17104  isreg2  17105  tgcmp  17128  hauscmplem  17133  hauscmp  17134  1stcfb  17171  1stcelcls  17187  lly1stc  17222  txcmplem1  17335  txlm  17342  xkococnlem  17353  filuni  17580  filufint  17615  ufilen  17625  fclscf  17720  metequiv2  18056  met1stc  18067  metrest  18070  xrsmopn  18318  xrge0tsms  18339  mulc1cncf  18409  cncfco  18411  cnheibor  18453  bndth  18456  lmmcvg  18687  cfil3i  18695  iscau4  18705  cmetcaulem  18714  iscmet3lem1  18717  caussi  18723  equivcfil  18725  equivcau  18726  caubl  18733  lmcau  18738  minveclem3b  18792  ovolgelb  18839  ovollb2lem  18847  ovolctb  18849  ovolicc2lem4  18879  ioombl1lem4  18918  dyadmax  18953  volsup2  18960  ismbf3d  19009  itg2monolem1  19105  c1liplem1  19343  c1lip1  19344  dvivthlem1  19355  lhop1  19361  ftc1a  19384  ftc1lem6  19388  ply1divex  19522  elply2  19578  dgrlem  19611  aacjcl  19707  aalioulem2  19713  aalioulem3  19714  aalioulem4  19715  ulmcaulem  19771  ulmcau  19772  ulmss  19774  ulmdvlem3  19779  mtest  19781  itgulm  19784  reeff1o  19823  efif1olem4  19907  rlimcnp  20260  xrlimcnp  20263  ftalem3  20312  fta  20317  muval1  20371  dvdssqf  20376  mumullem1  20417  pntlem3  20758  ostth  20788  grpoidinvlem3  20873  grpoideu  20876  grpoinveu  20889  isgrp2d  20902  rngo2  21055  ubthlem1  21449  minvecolem5  21460  htthlem  21497  pjhthlem2  21971  chscllem2  22217  nmopun  22594  lnconi  22613  rnbra  22687  sumdmdii  22995  cdj3lem2b  23017  reximddv  23028  xrofsup  23255  lmxrge0  23375  lmdvg  23376  xrge0tsmsd  23382  esumcvg  23454  indf1ofs  23609  cvmliftmolem2  23813  cvmliftlem15  23829  cvmlift2lem10  23843  cvmlift2lem12  23845  dedekind  24082  frmin  24242  nofulllem5  24360  axpasch  24569  btwndiff  24650  trisegint  24651  cgrxfr  24678  lineext  24699  segcon2  24728  brsegle2  24732  seglecgr12im  24733  segletr  24737  broutsideof3  24749  pdiveql  26168  abhp  26173  opnrebl2  26236  nn0prpw  26239  locfincmp  26304  sdclem1  26453  geomcau  26475  equivtotbnd  26502  bndss  26510  ismtybndlem  26530  heibor1lem  26533  rrncmslem  26556  prtlem15  26743  nacsfix  26787  fphpdo  26900  rencldnfilem  26903  irrapxlem2  26908  unxpwdom3  27256  psgneu  27429  expgrowth  27552  climinf  27732  stoweidlem7  27756  stoweidlem27  27776  stoweidlem39  27788  stoweidlem48  27797  stoweidlem49  27798  stoweidlem60  27809  stoweidlem61  27810  stoweid  27812  lsateln0  29185  lsat0cv  29223  eqlkr3  29291  lkrshp  29295  lshpset2N  29309  hlhgt2  29578  hlrelat2  29592  atle  29625  athgt  29645  2dim  29659  1cvratex  29662  ps-2  29667  dalem20  29882  lhpexle1lem  30196  lhpexle1  30197  lhpexle2lem  30198  lhpmcvr5N  30216  lhpmcvr6N  30217  cdleme25a  30542  cdleme29ex  30563  cdlemfnid  30753  cdlemg33b0  30890  cdlemg33a  30895  cdlemg35  30902  cdleml3N  31167  dihlsscpre  31424  dih1dimb2  31431  dihatexv  31528  dvh3dim2  31638  dochkr1  31668  dochkr1OLDN  31669  lcfl8  31692  lcfl8b  31694  lcfrlem5  31736  lcfrlem6  31737  mapdrvallem2  31835  mapdh9a  31980  mapdh9aOLDN  31981  hdmaprnlem3eN  32051  hdmaprnlem16N  32055
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator