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

Theorem reximdvai 2808
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 2806 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  reximdv  2809  reximdva  2810  reuind  3129  wefrc  4568  isomin  6048  isofrlem  6051  onfununi  6594  oaordex  6792  odi  6813  omass  6814  omeulem1  6816  noinfep  7603  rankwflemb  7708  infxpenlem  7884  coflim  8130  coftr  8142  zorn2lem7  8371  suplem1pr  8918  axpre-sup  9033  climbdd  12453  filufint  17940  grpoidinv  21784  cvati  23857  atcvat4i  23888  mdsymlem2  23895  mdsymlem3  23896  sumdmdii  23906  iccllyscon  24925  dftrpred3g  25491  incsequz2  26390  lcvat  29667  hlrelat3  30048  cvrval3  30049  cvrval4N  30050  2atlt  30075  cvrat4  30079  atbtwnexOLDN  30083  atbtwnex  30084  athgt  30092  2llnmat  30160  lnjatN  30416  2lnat  30420  cdlemb  30430  lhpexle3lem  30647  lhpex2leN  30649  cdlemf1  31197  cdlemf2  31198  cdlemf  31199  cdlemg1cex  31224  cdlemk26b-3  31541  dvh4dimlem  32080
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator