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

Theorem reximdvai 2624
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 2622 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 2517
This theorem is referenced by:  reximdv  2625  reximdva  2626  reuind  2917  wefrc  4324  isomin  5733  isofrlem  5736  onfununi  6291  oaordex  6489  odi  6510  omass  6511  omeulem1  6513  noinfep  7293  rankwflemb  7398  infxpenlem  7574  coflim  7820  coftr  7832  zorn2lem7  8062  suplem1pr  8609  axpre-sup  8724  filufint  17542  grpoidinv  20800  cvati  22871  atcvat4i  22902  mdsymlem2  22909  mdsymlem3  22910  sumdmdii  22920  iccllyscon  23118  dftrpred3g  23570  prl2  24501  cmptdst  24900  limptlimpr2lem1  24906  incsequz2  25791  lcvat  28350  hlrelat3  28731  cvrval3  28732  cvrval4N  28733  2atlt  28758  cvrat4  28762  atbtwnexOLDN  28766  atbtwnex  28767  athgt  28775  2llnmat  28843  lnjatN  29099  2lnat  29103  cdlemb  29113  lhpexle3lem  29330  lhpex2leN  29332  cdlemf1  29880  cdlemf2  29881  cdlemf  29882  cdlemg1cex  29907  cdlemk26b-3  30224  dvh4dimlem  30763
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 2520  df-rex 2521
  Copyright terms: Public domain W3C validator