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

Theorem reximdva 2754
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 424 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2752 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1717   E.wrex 2643
This theorem is referenced by:  wereu2  4513  dffo4  5817  nnaordex  6810  frfi  7281  fisupg  7284  marypha1  7367  wemapso2lem  7445  unwdomg  7478  noinfepOLD  7541  rankr1ai  7650  cofsmo  8075  cfcoflem  8078  inar1  8576  nqerf  8733  prlem936  8850  fimaxre  9880  arch  10143  bndndx  10145  zmin  10495  qbtwnxr  10711  qsqueeze  10712  qextltlem  10713  xrsupsslem  10810  xrinfmsslem  10811  xrub  10815  supxrunb1  10823  expnlbnd2  11430  r19.29uz  12074  cau3lem  12078  rlim2lt  12211  rlimclim  12260  2clim  12286  o1co  12300  climcn1  12305  climcn2  12306  rlimo1  12330  climsqz  12354  climsqz2  12355  rlimsqzlem  12362  lo1le  12365  climsup  12383  climcau  12384  caucvgrlem  12386  caucvgrlem2  12388  iseralt  12398  cvgcmp  12515  cvgcmpce  12517  supcvg  12555  rpnnen2  12745  bezoutlem1  12958  exprmfct  13030  isprm5  13032  pclem  13132  pc2dvds  13172  pcprmpw  13176  unbenlem  13196  infpnlem2  13199  infpn2  13201  prmunb  13202  vdwlem2  13270  ramub1lem2  13315  drsdirfi  14315  ipodrsima  14511  grpinveu  14759  odbezout  15114  sylow2blem3  15176  sylow2  15180  gexex  15388  irredrmul  15732  lsmelval2  16077  lbsextlem2  16151  znunit  16760  neiptopnei  17112  neitr  17159  cnpnei  17243  haust1  17331  nrmsep  17336  isnrm3  17338  regsep2  17355  isreg2  17356  tgcmp  17379  hauscmplem  17384  hauscmp  17385  1stcfb  17422  1stcelcls  17438  lly1stc  17473  txcmplem1  17587  txlm  17594  xkococnlem  17605  filuni  17831  filufint  17866  ufilen  17876  fclscf  17971  cnextcn  18012  ustex2sym  18160  ustex3sym  18161  utopreg  18196  isucn2  18223  ucnima  18225  ucncn  18229  neipcfilu  18240  metequiv2  18423  met1stc  18434  metrest  18437  xrsmopn  18707  xrge0tsms  18729  mulc1cncf  18799  cncfco  18801  cnheibor  18844  bndth  18847  lmmcvg  19078  cfil3i  19086  iscau4  19096  cmetcaulem  19105  iscmet3lem1  19108  caussi  19114  equivcfil  19116  equivcau  19117  caubl  19124  lmcau  19129  minveclem3b  19189  ovolgelb  19236  ovollb2lem  19244  ovolctb  19246  ovolicc2lem4  19276  ioombl1lem4  19315  dyadmax  19350  volsup2  19357  ismbf3d  19406  itg2monolem1  19502  c1liplem1  19740  c1lip1  19741  dvivthlem1  19752  lhop1  19758  ftc1a  19781  ftc1lem6  19785  ply1divex  19919  elply2  19975  dgrlem  20008  aacjcl  20104  aalioulem2  20110  aalioulem3  20111  aalioulem4  20112  ulmcaulem  20170  ulmcau  20171  ulmss  20173  ulmdvlem3  20178  mtest  20180  itgulm  20184  reeff1o  20223  efif1olem4  20307  rlimcnp  20664  xrlimcnp  20667  ftalem3  20717  fta  20722  muval1  20776  dvdssqf  20781  mumullem1  20822  pntlem3  21163  ostth  21193  grpoidinvlem3  21635  grpoideu  21638  grpoinveu  21651  isgrp2d  21664  rngo2  21817  ubthlem1  22213  minvecolem5  22224  htthlem  22261  pjhthlem2  22735  chscllem2  22981  nmopun  23358  lnconi  23377  rnbra  23451  sumdmdii  23759  cdj3lem2b  23781  reximddv  23799  xrofsup  23955  lmxrge0  24134  lmdvg  24135  esumlub  24241  esumfsup  24249  esumcvg  24265  lgamucov  24594  cvmliftmolem2  24741  cvmliftlem15  24757  cvmlift2lem10  24771  cvmlift2lem12  24773  dedekind  24959  frmin  25259  nofulllem5  25377  axpasch  25587  btwndiff  25668  trisegint  25669  cgrxfr  25696  lineext  25717  segcon2  25746  brsegle2  25750  seglecgr12im  25751  segletr  25755  broutsideof3  25767  itg2addnclem  25950  ftc1cnnc  25972  opnrebl2  26008  nn0prpw  26010  locfincmp  26068  sdclem1  26131  geomcau  26149  equivtotbnd  26171  bndss  26179  ismtybndlem  26199  heibor1lem  26202  rrncmslem  26225  prtlem15  26408  nacsfix  26450  fphpdo  26562  rencldnfilem  26565  irrapxlem2  26570  unxpwdom3  26918  psgneu  27091  expgrowth  27214  climinf  27393  stoweidlem7  27417  stoweidlem27  27437  stoweidlem39  27449  stoweidlem48  27458  stoweidlem49  27459  stoweidlem60  27470  stoweidlem61  27471  stoweid  27473  2pthfrgrarn2  27756  frgrawopreglem5  27793  lsateln0  29161  lsat0cv  29199  eqlkr3  29267  lkrshp  29271  lshpset2N  29285  hlhgt2  29554  hlrelat2  29568  atle  29601  athgt  29621  2dim  29635  1cvratex  29638  ps-2  29643  dalem20  29858  lhpexle1lem  30172  lhpexle1  30173  lhpexle2lem  30174  lhpmcvr5N  30192  lhpmcvr6N  30193  cdleme25a  30518  cdleme29ex  30539  cdlemfnid  30729  cdlemg33b0  30866  cdlemg33a  30871  cdlemg35  30878  cdleml3N  31143  dihlsscpre  31400  dih1dimb2  31407  dihatexv  31504  dvh3dim2  31614  dochkr1  31644  dochkr1OLDN  31645  lcfl8  31668  lcfl8b  31670  lcfrlem5  31712  lcfrlem6  31713  mapdrvallem2  31811  mapdh9a  31956  mapdh9aOLDN  31957  hdmaprnlem3eN  32027  hdmaprnlem16N  32031
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2647  df-rex 2648
  Copyright terms: Public domain W3C validator