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

Theorem reximdva 2668
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 2666 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 1696   E.wrex 2557
This theorem is referenced by:  wereu2  4406  dffo4  5692  nnaordex  6652  frfi  7118  fisupg  7121  marypha1  7203  wemapso2lem  7281  unwdomg  7314  noinfepOLD  7377  rankr1ai  7486  cofsmo  7911  cfcoflem  7914  inar1  8413  nqerf  8570  prlem936  8687  fimaxre  9717  arch  9978  bndndx  9980  zmin  10328  qbtwnxr  10543  qsqueeze  10544  qextltlem  10545  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrunb1  10654  expnlbnd2  11248  r19.29uz  11850  cau3lem  11854  rlim2lt  11987  rlimclim  12036  2clim  12062  o1co  12076  climcn1  12081  climcn2  12082  rlimo1  12106  climsqz  12130  climsqz2  12131  rlimsqzlem  12138  lo1le  12141  climsup  12159  climcau  12160  caucvgrlem  12161  caucvgrlem2  12163  iseralt  12173  cvgcmp  12290  cvgcmpce  12292  supcvg  12330  rpnnen2  12520  bezoutlem1  12733  exprmfct  12805  isprm5  12807  pclem  12907  pc2dvds  12947  pcprmpw  12951  unbenlem  12971  infpnlem2  12974  infpn2  12976  prmunb  12977  vdwlem2  13045  ramub1lem2  13090  drsdirfi  14088  ipodrsima  14284  grpinveu  14532  odbezout  14887  sylow2blem3  14949  sylow2  14953  gexex  15161  irredrmul  15505  lsmelval2  15854  lbsextlem2  15928  znunit  16533  cnpnei  17009  haust1  17096  nrmsep  17101  isnrm3  17103  regsep2  17120  isreg2  17121  tgcmp  17144  hauscmplem  17149  hauscmp  17150  1stcfb  17187  1stcelcls  17203  lly1stc  17238  txcmplem1  17351  txlm  17358  xkococnlem  17369  filuni  17596  filufint  17631  ufilen  17641  fclscf  17736  metequiv2  18072  met1stc  18083  metrest  18086  xrsmopn  18334  xrge0tsms  18355  mulc1cncf  18425  cncfco  18427  cnheibor  18469  bndth  18472  lmmcvg  18703  cfil3i  18711  iscau4  18721  cmetcaulem  18730  iscmet3lem1  18733  caussi  18739  equivcfil  18741  equivcau  18742  caubl  18749  lmcau  18754  minveclem3b  18808  ovolgelb  18855  ovollb2lem  18863  ovolctb  18865  ovolicc2lem4  18895  ioombl1lem4  18934  dyadmax  18969  volsup2  18976  ismbf3d  19025  itg2monolem1  19121  c1liplem1  19359  c1lip1  19360  dvivthlem1  19371  lhop1  19377  ftc1a  19400  ftc1lem6  19404  ply1divex  19538  elply2  19594  dgrlem  19627  aacjcl  19723  aalioulem2  19729  aalioulem3  19730  aalioulem4  19731  ulmcaulem  19787  ulmcau  19788  ulmss  19790  ulmdvlem3  19795  mtest  19797  itgulm  19800  reeff1o  19839  efif1olem4  19923  rlimcnp  20276  xrlimcnp  20279  ftalem3  20328  fta  20333  muval1  20387  dvdssqf  20392  mumullem1  20433  pntlem3  20774  ostth  20804  grpoidinvlem3  20889  grpoideu  20892  grpoinveu  20905  isgrp2d  20918  rngo2  21071  ubthlem1  21465  minvecolem5  21476  htthlem  21513  pjhthlem2  21987  chscllem2  22233  nmopun  22610  lnconi  22629  rnbra  22703  sumdmdii  23011  cdj3lem2b  23033  reximddv  23044  xrofsup  23270  lmxrge0  23390  lmdvg  23391  xrge0tsmsd  23397  esumcvg  23469  indf1ofs  23624  cvmliftmolem2  23828  cvmliftlem15  23844  cvmlift2lem10  23858  cvmlift2lem12  23860  dedekind  24097  frmin  24313  nofulllem5  24431  axpasch  24641  btwndiff  24722  trisegint  24723  cgrxfr  24750  lineext  24771  segcon2  24800  brsegle2  24804  seglecgr12im  24805  segletr  24809  broutsideof3  24821  itg2addnclem  25003  ftc1cnnc  25025  pdiveql  26271  abhp  26276  opnrebl2  26339  nn0prpw  26342  locfincmp  26407  sdclem1  26556  geomcau  26578  equivtotbnd  26605  bndss  26613  ismtybndlem  26633  heibor1lem  26636  rrncmslem  26659  prtlem15  26846  nacsfix  26890  fphpdo  27003  rencldnfilem  27006  irrapxlem2  27011  unxpwdom3  27359  psgneu  27532  expgrowth  27655  climinf  27835  stoweidlem7  27859  stoweidlem27  27879  stoweidlem39  27891  stoweidlem48  27900  stoweidlem49  27901  stoweidlem60  27912  stoweidlem61  27913  stoweid  27915  2pthfrgrarn2  28434  lsateln0  29807  lsat0cv  29845  eqlkr3  29913  lkrshp  29917  lshpset2N  29931  hlhgt2  30200  hlrelat2  30214  atle  30247  athgt  30267  2dim  30281  1cvratex  30284  ps-2  30289  dalem20  30504  lhpexle1lem  30818  lhpexle1  30819  lhpexle2lem  30820  lhpmcvr5N  30838  lhpmcvr6N  30839  cdleme25a  31164  cdleme29ex  31185  cdlemfnid  31375  cdlemg33b0  31512  cdlemg33a  31517  cdlemg35  31524  cdleml3N  31789  dihlsscpre  32046  dih1dimb2  32053  dihatexv  32150  dvh3dim2  32260  dochkr1  32290  dochkr1OLDN  32291  lcfl8  32314  lcfl8b  32316  lcfrlem5  32358  lcfrlem6  32359  mapdrvallem2  32457  mapdh9a  32602  mapdh9aOLDN  32603  hdmaprnlem3eN  32673  hdmaprnlem16N  32677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator