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

Theorem reximdva 2858
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 441 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2856 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    e. wcel 1904   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-ral 2761  df-rex 2762
This theorem is referenced by:  reximddv  2859  reximddv2  2860  wereu2  4836  dffo4  6053  nnaordex  7357  frfi  7834  fisupg  7837  marypha1  7966  fiinfg  8033  wemapsolem  8083  unwdomg  8117  rankr1ai  8287  cofsmo  8717  cfcoflem  8720  inar1  9218  nqerf  9373  prlem936  9490  fimaxre  10573  arch  10890  bndndx  10892  suprfinzcl  11073  zmin  11283  qbtwnxr  11516  qsqueeze  11517  qextltlem  11518  xrsupsslem  11617  xrinfmsslem  11618  xrub  11622  supxrunb1  11630  ssnn0fi  12235  fsuppmapnn0fiub0  12243  fsuppmapnn0fz  12246  expnlbnd2  12441  r19.29uz  13490  cau3lem  13494  rlim2lt  13638  rlimclim  13687  2clim  13713  o1co  13727  climcn1  13732  climcn2  13733  rlimo1  13757  climsqz  13781  climsqz2  13782  rlimsqzlem  13789  lo1le  13792  climsup  13810  climcau  13811  caucvgrlem2  13817  iseralt  13828  cvgcmp  13953  cvgcmpce  13955  supcvg  13991  rpnnen2  14355  bezoutlem1  14582  lcmgcdlem  14650  exprmfct  14727  prmdvdsfz  14728  pclem  14867  pc2dvds  14907  pcprmpw  14911  unbenlem  14931  infpnlem2  14934  infpn2  14936  prmunb  14937  vdwlem2  15011  ramub1lem2  15064  prmdvdsprmop  15080  prmdvdsprmorpOLD  15095  prmgaplem7  15106  ipodrsima  16489  grpinveu  16778  psgneu  17225  odbezout  17287  sylow2blem3  17352  nn0gsumfz  17691  irredrmul  18013  lsmelval2  18386  lbsextlem2  18460  mptcoe1fsupp  18885  znunit  19211  scmate  19612  scmatscm  19615  scmatfo  19632  mat1scmat  19641  pmatcoe1fsupp  19802  pmatcollpwfi  19883  pmatcollpw3fi  19886  mptcoe1matfsupp  19903  pm2mp  19926  chmaidscmat  19949  cpmadugsum  19979  cpmadumatpoly  19984  chcoeffeq  19987  cayhamlem3  19988  cayhamlem4  19989  neiptopnei  20225  neitr  20273  cnpnei  20357  haust1  20445  isnrm3  20452  isreg2  20470  tgcmp  20493  hauscmplem  20498  hauscmp  20499  bwth  20502  1stcfb  20537  1stcelcls  20553  lly1stc  20588  txcmplem1  20733  txlm  20740  xkococnlem  20751  filuni  20978  filufint  21013  ufilen  21023  fclscf  21118  cnextcn  21160  ustex2sym  21309  ustex3sym  21310  utopreg  21345  isucn2  21372  ucnima  21374  ucncn  21378  neipcfilu  21389  metequiv2  21603  metrest  21617  xrsmopn  21908  mulc1cncf  22015  cncfco  22017  bndth  22064  lmmcvg  22309  cfil3i  22317  iscau4  22327  cmetcaulem  22336  iscmet3lem1  22339  caussi  22345  equivcfil  22347  equivcau  22348  caubl  22355  minveclem3b  22448  minveclem3bOLD  22460  ovolgelb  22511  ovollb2lem  22519  ovolctb  22521  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ioombl1lem4  22593  dyadmax  22635  volsup2  22642  itg2monolem1  22787  c1liplem1  23027  c1lip1  23028  dvivthlem1  23039  lhop1  23045  ftc1a  23068  ftc1lem6  23072  ply1divex  23166  elply2  23229  dgrlem  23262  aacjcl  23362  aalioulem2  23368  aalioulem3  23369  aalioulem4  23370  ulmcaulem  23428  ulmcau  23429  ulmss  23431  mtest  23438  itgulm  23442  reeff1o  23481  efif1olem4  23573  rlimcnp  23970  xrlimcnp  23973  lgamucov  24042  ftalem3  24078  fta  24085  muval1  24139  dvdssqf  24144  mumullem1  24185  pntlem3  24526  ostth  24556  tgtrisegint  24622  tgbtwndiff  24629  tgcgrxfr  24642  lnext  24691  legov2  24710  legtrd  24713  hlcgrex  24740  colperpexlem3  24853  colperpex  24854  hlpasch  24877  hpgerlem  24886  hpgtr  24889  dfcgra2  24950  acopy  24953  inagswap  24959  inaghl  24960  cgrg3col4  24963  axpasch  25050  wwlknredwwlkn0  25534  2pthfrgrarn2  25817  frgrawopreglem5  25855  usgreg2spot  25874  grpoidinvlem3  26015  grpoideu  26018  grpoinveu  26031  isgrp2d  26044  rngo2  26197  ubthlem1  26593  minvecolem5  26604  minvecolem5OLD  26614  htthlem  26651  chscllem2  27372  nmopun  27748  lnconi  27767  rnbra  27841  sumdmdii  28149  cdj3lem2b  28171  foresf1o  28218  acunirnmpt  28336  xrofsup  28428  isarchi3  28578  isarchiofld  28654  lmxrge0  28832  lmdvg  28833  esumlub  28955  esumfsup  28965  esumcvg  28981  eulerpartlemgvv  29282  cvmliftmolem2  30077  cvmlift2lem10  30107  cvmlift2lem12  30109  frmin  30551  wzel  30578  wsuclem  30579  nofulllem5  30666  btwndiff  30865  trisegint  30866  cgrxfr  30893  lineext  30914  segcon2  30943  brsegle2  30947  seglecgr12im  30948  segletr  30952  broutsideof3  30964  opnrebl2  31048  nn0prpw  31050  fin2so  31996  poimirlem27  32031  poimirlem30  32034  poimirlem31  32035  poimir  32037  mblfinlem1  32041  mblfinlem2  32042  mblfinlem3  32043  mblfinlem4  32044  itg2addnclem  32057  ftc1cnnc  32080  ftc1anclem5  32085  ftc1anclem6  32086  sdclem1  32136  geomcau  32152  equivtotbnd  32174  bndss  32182  ismtybndlem  32202  heibor1lem  32205  rrncmslem  32228  prtlem15  32511  lsateln0  32632  lsat0cv  32670  eqlkr3  32738  lkrshp  32742  lshpset2N  32756  hlhgt2  33025  hlrelat2  33039  atle  33072  athgt  33092  2dim  33106  1cvratex  33109  ps-2  33114  dalem20  33329  lhpexle1lem  33643  lhpexle1  33644  lhpexle2lem  33645  lhpmcvr5N  33663  lhpmcvr6N  33664  cdleme25a  33991  cdleme29ex  34012  cdlemfnid  34202  cdlemg33b0  34339  cdlemg33a  34344  cdlemg35  34351  cdleml3N  34616  dihlsscpre  34873  dih1dimb2  34880  dihatexv  34977  dvh3dim2  35087  dochkr1  35117  dochkr1OLDN  35118  lcfl8  35141  lcfl8b  35143  lcfrlem5  35185  lcfrlem6  35186  mapdrvallem2  35284  mapdh9a  35429  mapdh9aOLDN  35430  hdmaprnlem3eN  35500  hdmaprnlem16N  35504  fphpdo  35731  rencldnfilem  35734  irrapxlem2  35738  cvgdvgrat  36732  expgrowth  36754  projf1o  37545  ssfiunibd  37615  supxrgere  37643  supxrgelem  37647  suplesup  37649  infrpge  37661  infleinf  37682  qinioo  37733  climinf  37781  climinfOLD  37782  mullimc  37793  islptre  37796  limccog  37797  mullimcf  37800  limcrecl  37806  sumnnodd  37807  neglimc  37825  0ellimcdiv  37827  limclner  37829  cncfioobd  37872  stoweidlem7  37979  stoweidlem27  37999  stoweidlem39  38012  stoweidlem48  38021  stoweidlem49  38022  stoweidlem60  38033  stoweidlem61  38034  stoweid  38037  dirkercncflem2  38078  fourierdlem20  38101  fourierdlem39  38121  fourierdlem41  38123  fourierdlem48  38130  fourierdlem49  38131  fourierdlem50  38132  fourierdlem64  38146  fourierdlem73  38155  fourierdlem74  38156  fourierdlem75  38157  fourierdlem87  38169  fourierdlem103  38185  fourierdlem104  38186  qndenserrnopnlem  38278  sge0ltfirp  38356  sge0gerpmpt  38358  sge0ltfirpmpt2  38382  sge0isum  38383  sge0pnffigtmpt  38396  sge0pnffsumgt  38398  sge0gtfsumgt  38399  sge0uzfsumgt  38400  nnfoctbdjlem  38409  omeiunltfirp  38459  carageniuncllem2  38462  hoicvr  38488  volicorescl  38493  hoidmv1le  38534  hoidmvlelem3  38537  hoiqssbllem3  38564  hspmbllem2  38567  bgoldbwt  39023  bgoldbst  39024  sgoldbalt  39027  bgoldbtbndlem4  39048  bgoldbtbnd  39049  proththd  39059  zrninitoringc  40581  ply1mulgsumlem3  40688  ply1mulgsumlem4  40689  islindeps2  40784  isldepslvec2  40786
  Copyright terms: Public domain W3C validator