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

Theorem reximdva 2818
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 2816 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 1725   E.wrex 2706
This theorem is referenced by:  wereu2  4579  dffo4  5885  nnaordex  6881  frfi  7352  fisupg  7355  marypha1  7439  wemapso2lem  7519  unwdomg  7552  noinfepOLD  7615  rankr1ai  7724  cofsmo  8149  cfcoflem  8152  inar1  8650  nqerf  8807  prlem936  8924  fimaxre  9955  arch  10218  bndndx  10220  zmin  10570  qbtwnxr  10786  qsqueeze  10787  qextltlem  10788  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  supxrunb1  10898  expnlbnd2  11510  r19.29uz  12154  cau3lem  12158  rlim2lt  12291  rlimclim  12340  2clim  12366  o1co  12380  climcn1  12385  climcn2  12386  rlimo1  12410  climsqz  12434  climsqz2  12435  rlimsqzlem  12442  lo1le  12445  climsup  12463  climcau  12464  caucvgrlem  12466  caucvgrlem2  12468  iseralt  12478  cvgcmp  12595  cvgcmpce  12597  supcvg  12635  rpnnen2  12825  bezoutlem1  13038  exprmfct  13110  isprm5  13112  pclem  13212  pc2dvds  13252  pcprmpw  13256  unbenlem  13276  infpnlem2  13279  infpn2  13281  prmunb  13282  vdwlem2  13350  ramub1lem2  13395  drsdirfi  14395  ipodrsima  14591  grpinveu  14839  odbezout  15194  sylow2blem3  15256  sylow2  15260  gexex  15468  irredrmul  15812  lsmelval2  16157  lbsextlem2  16231  znunit  16844  neiptopnei  17196  neitr  17244  cnpnei  17328  haust1  17416  nrmsep  17421  isnrm3  17423  regsep2  17440  isreg2  17441  tgcmp  17464  hauscmplem  17469  hauscmp  17470  1stcfb  17508  1stcelcls  17524  lly1stc  17559  txcmplem1  17673  txlm  17680  xkococnlem  17691  filuni  17917  filufint  17952  ufilen  17962  fclscf  18057  cnextcn  18098  ustex2sym  18246  ustex3sym  18247  utopreg  18282  isucn2  18309  ucnima  18311  ucncn  18315  neipcfilu  18326  metequiv2  18540  met1stc  18551  metrest  18554  xrsmopn  18843  xrge0tsms  18865  mulc1cncf  18935  cncfco  18937  cnheibor  18980  bndth  18983  lmmcvg  19214  cfil3i  19222  iscau4  19232  cmetcaulem  19241  iscmet3lem1  19244  caussi  19250  equivcfil  19252  equivcau  19253  caubl  19260  lmcau  19265  minveclem3b  19329  ovolgelb  19376  ovollb2lem  19384  ovolctb  19386  ovolicc2lem4  19416  ioombl1lem4  19455  dyadmax  19490  volsup2  19497  ismbf3d  19546  itg2monolem1  19642  c1liplem1  19880  c1lip1  19881  dvivthlem1  19892  lhop1  19898  ftc1a  19921  ftc1lem6  19925  ply1divex  20059  elply2  20115  dgrlem  20148  aacjcl  20244  aalioulem2  20250  aalioulem3  20251  aalioulem4  20252  ulmcaulem  20310  ulmcau  20311  ulmss  20313  ulmdvlem3  20318  mtest  20320  itgulm  20324  reeff1o  20363  efif1olem4  20447  rlimcnp  20804  xrlimcnp  20807  ftalem3  20857  fta  20862  muval1  20916  dvdssqf  20921  mumullem1  20962  pntlem3  21303  ostth  21333  grpoidinvlem3  21794  grpoideu  21797  grpoinveu  21810  isgrp2d  21823  rngo2  21976  ubthlem1  22372  minvecolem5  22383  htthlem  22420  pjhthlem2  22894  chscllem2  23140  nmopun  23517  lnconi  23536  rnbra  23610  sumdmdii  23918  cdj3lem2b  23940  reximddv  23962  xrofsup  24126  lmxrge0  24337  lmdvg  24338  esumlub  24452  esumfsup  24460  esumcvg  24476  lgamucov  24822  cvmliftmolem2  24969  cvmliftlem15  24985  cvmlift2lem10  24999  cvmlift2lem12  25001  dedekind  25187  frmin  25517  wzel  25575  wsuclem  25576  nofulllem5  25661  axpasch  25880  btwndiff  25961  trisegint  25962  cgrxfr  25989  lineext  26010  segcon2  26039  brsegle2  26043  seglecgr12im  26044  segletr  26048  broutsideof3  26060  mblfinlem1  26243  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  itg2addnclem  26256  ftc1cnnc  26279  ftc1anclem5  26284  ftc1anclem6  26285  opnrebl2  26324  nn0prpw  26326  locfincmp  26384  sdclem1  26447  geomcau  26465  equivtotbnd  26487  bndss  26495  ismtybndlem  26515  heibor1lem  26518  rrncmslem  26541  prtlem15  26724  nacsfix  26766  fphpdo  26878  rencldnfilem  26881  irrapxlem2  26886  unxpwdom3  27233  psgneu  27406  expgrowth  27529  climinf  27708  stoweidlem7  27732  stoweidlem27  27752  stoweidlem39  27764  stoweidlem48  27773  stoweidlem49  27774  stoweidlem60  27785  stoweidlem61  27786  stoweid  27788  2pthfrgrarn2  28400  frgrawopreglem5  28437  usgreg2spot  28456  lsateln0  29793  lsat0cv  29831  eqlkr3  29899  lkrshp  29903  lshpset2N  29917  hlhgt2  30186  hlrelat2  30200  atle  30233  athgt  30253  2dim  30267  1cvratex  30270  ps-2  30275  dalem20  30490  lhpexle1lem  30804  lhpexle1  30805  lhpexle2lem  30806  lhpmcvr5N  30824  lhpmcvr6N  30825  cdleme25a  31150  cdleme29ex  31171  cdlemfnid  31361  cdlemg33b0  31498  cdlemg33a  31503  cdlemg35  31510  cdleml3N  31775  dihlsscpre  32032  dih1dimb2  32039  dihatexv  32136  dvh3dim2  32246  dochkr1  32276  dochkr1OLDN  32277  lcfl8  32300  lcfl8b  32302  lcfrlem5  32344  lcfrlem6  32345  mapdrvallem2  32443  mapdh9a  32588  mapdh9aOLDN  32589  hdmaprnlem3eN  32659  hdmaprnlem16N  32663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2710  df-rex 2711
  Copyright terms: Public domain W3C validator