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

Theorem reximdvai 2615
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 2613 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 2510
This theorem is referenced by:  reximdv  2616  reximdva  2617  reuind  2903  wefrc  4280  isomin  5686  isofrlem  5689  onfununi  6244  oaordex  6442  odi  6463  omass  6464  omeulem1  6466  noinfep  7244  rankwflemb  7349  infxpenlem  7525  coflim  7771  coftr  7783  zorn2lem7  8013  suplem1pr  8556  axpre-sup  8671  filufint  17447  grpoidinv  20705  cvati  22776  atcvat4i  22807  mdsymlem2  22814  mdsymlem3  22815  sumdmdii  22825  iccllyscon  22952  dftrpred3g  23404  prl2  24335  cmptdst  24734  limptlimpr2lem1  24740  incsequz2  25625  lcvat  27979  hlrelat3  28360  cvrval3  28361  cvrval4N  28362  2atlt  28387  cvrat4  28391  atbtwnexOLDN  28395  atbtwnex  28396  athgt  28404  2llnmat  28472  lnjatN  28728  2lnat  28732  cdlemb  28742  lhpexle3lem  28959  lhpex2leN  28961  cdlemf1  29509  cdlemf2  29510  cdlemf  29511  cdlemg1cex  29536  cdlemk26b-3  29853  dvh4dimlem  30392
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 2513  df-rex 2514
  Copyright terms: Public domain W3C validator