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

Theorem reximdvai 2666
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 1609 . 2  |-  F/ x ph
2 reximdvai.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
31, 2reximdai 2664 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  reximdv  2667  reximdva  2668  reuind  2981  wefrc  4403  isomin  5850  isofrlem  5853  onfununi  6374  oaordex  6572  odi  6593  omass  6594  omeulem1  6596  noinfep  7376  rankwflemb  7481  infxpenlem  7657  coflim  7903  coftr  7915  zorn2lem7  8145  suplem1pr  8692  axpre-sup  8807  filufint  17631  grpoidinv  20891  cvati  22962  atcvat4i  22993  mdsymlem2  23000  mdsymlem3  23001  sumdmdii  23011  iccllyscon  23796  dftrpred3g  24307  prl2  25272  cmptdst  25671  limptlimpr2lem1  25677  incsequz2  26562  lcvat  29842  hlrelat3  30223  cvrval3  30224  cvrval4N  30225  2atlt  30250  cvrat4  30254  atbtwnexOLDN  30258  atbtwnex  30259  athgt  30267  2llnmat  30335  lnjatN  30591  2lnat  30595  cdlemb  30605  lhpexle3lem  30822  lhpex2leN  30824  cdlemf1  31372  cdlemf2  31373  cdlemf  31374  cdlemg1cex  31399  cdlemk26b-3  31716  dvh4dimlem  32255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator