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

Theorem ralimdv 2624
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
Hypothesis
Ref Expression
ralimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ralimdv  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ralimdv
StepHypRef Expression
1 ralimdv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21adantr 453 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32ralimdva 2623 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1685   A.wral 2545
This theorem is referenced by:  poss  4316  sess1  4361  sess2  4362  tfindsg  4651  riinint  4935  iinpreima  5617  dffo4  5638  dffo5  5639  isoini2  5798  abianfp  6467  iiner  6727  xpf1o  7019  dffi3  7180  brwdom3  7292  xpwdomg  7295  bndrank  7509  cfub  7871  cff1  7880  cfflb  7881  cfslb2n  7890  cofsmo  7891  cfcoflem  7894  pwcfsdom  8201  fpwwe2lem13  8260  inawinalem  8307  grupr  8415  fsequb  11032  cau3lem  11833  caubnd2  11836  caubnd  11837  rlim2lt  11966  rlim3  11967  climshftlem  12043  isercolllem1  12133  climcau  12139  caucvgb  12147  serf0  12148  cvgcmp  12269  mreriincl  13495  acsfn1c  13559  islss4  15714  riinopn  16649  fiinbas  16685  baspartn  16687  isclo2  16820  lmcls  17025  lmcnp  17027  isnrm3  17082  1stcelcls  17182  llyss  17200  nllyss  17201  ptpjpre1  17261  txlly  17325  txnlly  17326  tx1stc  17339  xkococnlem  17348  fbunfip  17559  filssufilg  17601  cnpflf2  17690  fcfnei  17725  rescncf  18396  lebnum  18457  cfilss  18691  fgcfil  18692  iscau4  18700  cmetcaulem  18709  cfilres  18717  caussi  18718  ovolunlem1  18851  ulmclm  19761  ulmcaulem  19766  ulmcau  19767  ulmss  19769  rlimcnp  20255  cxploglim  20267  lgsdchr  20582  pntlemp  20754  nmlnoubi  21367  lnon0  21369  iccllyscon  23186  cvmlift2lem1  23238  setlikess  23597  axcontlem4  24003  ab2rexex2g  24532  prltub  24660  tolat  24686  latdir  24695  svli2  24884  lemindclsbu  25395  indcls2  25396  upixp  25803  caushft  25877  sstotbnd3  25900  totbndss  25901  unichnidl  26056  ispridl2  26063  elrfirn2  26171  mzpsubst  26226  eluzrabdioph  26287
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1533  df-ral 2550
  Copyright terms: Public domain W3C validator