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

Theorem reximdvai 2628
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 2626 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 2519
This theorem is referenced by:  reximdv  2629  reximdva  2630  reuind  2943  wefrc  4359  isomin  5768  isofrlem  5771  onfununi  6326  oaordex  6524  odi  6545  omass  6546  omeulem1  6548  noinfep  7328  rankwflemb  7433  infxpenlem  7609  coflim  7855  coftr  7867  zorn2lem7  8097  suplem1pr  8644  axpre-sup  8759  filufint  17577  grpoidinv  20835  cvati  22906  atcvat4i  22937  mdsymlem2  22944  mdsymlem3  22945  sumdmdii  22955  iccllyscon  23153  dftrpred3g  23605  prl2  24536  cmptdst  24935  limptlimpr2lem1  24941  incsequz2  25826  lcvat  28387  hlrelat3  28768  cvrval3  28769  cvrval4N  28770  2atlt  28795  cvrat4  28799  atbtwnexOLDN  28803  atbtwnex  28804  athgt  28812  2llnmat  28880  lnjatN  29136  2lnat  29140  cdlemb  29150  lhpexle3lem  29367  lhpex2leN  29369  cdlemf1  29917  cdlemf2  29918  cdlemf  29919  cdlemg1cex  29944  cdlemk26b-3  30261  dvh4dimlem  30800
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 2523  df-rex 2524
  Copyright terms: Public domain W3C validator