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

Theorem reximdvai 2656
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 groups:    ps( x)    ch( x)    A( x)

Proof of Theorem reximdvai
StepHypRef Expression
1 nfv 1607 . 2  |-  F/ x ph
2 reximdvai.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
31, 2reximdai 2654 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1687   E.wrex 2547
This theorem is referenced by:  reximdv  2657  reximdva  2658  reuind  2971  wefrc  4388  isomin  5797  isofrlem  5800  onfununi  6355  oaordex  6553  odi  6574  omass  6575  omeulem1  6577  noinfep  7357  rankwflemb  7462  infxpenlem  7638  coflim  7884  coftr  7896  zorn2lem7  8126  suplem1pr  8673  axpre-sup  8788  filufint  17611  grpoidinv  20869  cvati  22940  atcvat4i  22971  mdsymlem2  22978  mdsymlem3  22979  sumdmdii  22989  iccllyscon  23187  dftrpred3g  23639  prl2  24570  cmptdst  24969  limptlimpr2lem1  24975  incsequz2  25860  lcvat  28489  hlrelat3  28870  cvrval3  28871  cvrval4N  28872  2atlt  28897  cvrat4  28901  atbtwnexOLDN  28905  atbtwnex  28906  athgt  28914  2llnmat  28982  lnjatN  29238  2lnat  29242  cdlemb  29252  lhpexle3lem  29469  lhpex2leN  29471  cdlemf1  30019  cdlemf2  30020  cdlemf  30021  cdlemg1cex  30046  cdlemk26b-3  30363  dvh4dimlem  30902
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-11 1718
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1531  df-nf 1534  df-ral 2551  df-rex 2552
  Copyright terms: Public domain W3C validator