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  23781  dftrpred3g  24236  prl2  25169  cmptdst  25568  limptlimpr2lem1  25574  incsequz2  26459  lcvat  29220  hlrelat3  29601  cvrval3  29602  cvrval4N  29603  2atlt  29628  cvrat4  29632  atbtwnexOLDN  29636  atbtwnex  29637  athgt  29645  2llnmat  29713  lnjatN  29969  2lnat  29973  cdlemb  29983  lhpexle3lem  30200  lhpex2leN  30202  cdlemf1  30750  cdlemf2  30751  cdlemf  30752  cdlemg1cex  30777  cdlemk26b-3  31094  dvh4dimlem  31633
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