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

Theorem reximdvai 2653
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 1605 . 2  |-  F/ x ph
2 reximdvai.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
31, 2reximdai 2651 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  reximdv  2654  reximdva  2655  reuind  2968  wefrc  4387  isomin  5834  isofrlem  5837  onfununi  6358  oaordex  6556  odi  6577  omass  6578  omeulem1  6580  noinfep  7360  rankwflemb  7465  infxpenlem  7641  coflim  7887  coftr  7899  zorn2lem7  8129  suplem1pr  8676  axpre-sup  8791  filufint  17615  grpoidinv  20875  cvati  22946  atcvat4i  22977  mdsymlem2  22984  mdsymlem3  22985  sumdmdii  22995  iccllyscon  23192  dftrpred3g  23647  prl2  24581  cmptdst  24980  limptlimpr2lem1  24986  incsequz2  25871  lcvat  28593  hlrelat3  28974  cvrval3  28975  cvrval4N  28976  2atlt  29001  cvrat4  29005  atbtwnexOLDN  29009  atbtwnex  29010  athgt  29018  2llnmat  29086  lnjatN  29342  2lnat  29346  cdlemb  29356  lhpexle3lem  29573  lhpex2leN  29575  cdlemf1  30123  cdlemf2  30124  cdlemf  30125  cdlemg1cex  30150  cdlemk26b-3  30467  dvh4dimlem  31006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator