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

Theorem reximdvai 2615
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.)
Hypothesis
Ref Expression
reximdvai.1  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
reximdvai  |-  ( 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 reximdvai
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 reximdvai.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
31, 2reximdai 2613 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   E.wrex 2510
This theorem is referenced by:  reximdv  2616  reximdva  2617  reuind  2903  wefrc  4280  isomin  5686  isofrlem  5689  onfununi  6244  oaordex  6442  odi  6463  omass  6464  omeulem1  6466  noinfep  7244  rankwflemb  7349  infxpenlem  7525  coflim  7771  coftr  7783  zorn2lem7  8013  suplem1pr  8556  axpre-sup  8671  filufint  17447  grpoidinv  20705  cvati  22776  atcvat4i  22807  mdsymlem2  22814  mdsymlem3  22815  sumdmdii  22825  iccllyscon  22952  dftrpred3g  23404  prl2  24335  cmptdst  24734  limptlimpr2lem1  24740  incsequz2  25625  lcvat  27909  hlrelat3  28290  cvrval3  28291  cvrval4N  28292  2atlt  28317  cvrat4  28321  atbtwnexOLDN  28325  atbtwnex  28326  athgt  28334  2llnmat  28402  lnjatN  28658  2lnat  28662  cdlemb  28672  lhpexle3lem  28889  lhpex2leN  28891  cdlemf1  29439  cdlemf2  29440  cdlemf  29441  cdlemg1cex  29466  cdlemk26b-3  29783  dvh4dimlem  30322
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator