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

Theorem ralimdv 2622
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 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32ralimdva 2621 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543
This theorem is referenced by:  poss  4316  sess1  4361  sess2  4362  tfindsg  4651  riinint  4935  iinpreima  5655  dffo4  5676  dffo5  5677  isoini2  5836  abianfp  6471  iiner  6731  xpf1o  7023  dffi3  7184  brwdom3  7296  xpwdomg  7299  bndrank  7513  cfub  7875  cff1  7884  cfflb  7885  cfslb2n  7894  cofsmo  7895  cfcoflem  7898  pwcfsdom  8205  fpwwe2lem13  8264  inawinalem  8311  grupr  8419  fsequb  11037  cau3lem  11838  caubnd2  11841  caubnd  11842  rlim2lt  11971  rlim3  11972  climshftlem  12048  isercolllem1  12138  climcau  12144  caucvgb  12152  serf0  12153  cvgcmp  12274  mreriincl  13500  acsfn1c  13564  islss4  15719  riinopn  16654  fiinbas  16690  baspartn  16692  isclo2  16825  lmcls  17030  lmcnp  17032  isnrm3  17087  1stcelcls  17187  llyss  17205  nllyss  17206  ptpjpre1  17266  txlly  17330  txnlly  17331  tx1stc  17344  xkococnlem  17353  fbunfip  17564  filssufilg  17606  cnpflf2  17695  fcfnei  17730  rescncf  18401  lebnum  18462  cfilss  18696  fgcfil  18697  iscau4  18705  cmetcaulem  18714  cfilres  18722  caussi  18723  ovolunlem1  18856  ulmclm  19766  ulmcaulem  19771  ulmcau  19772  ulmss  19774  rlimcnp  20260  cxploglim  20272  lgsdchr  20587  pntlemp  20759  nmlnoubi  21374  lnon0  21376  disjpreima  23361  iccllyscon  23781  cvmlift2lem1  23833  setlikess  24195  axcontlem4  24595  ab2rexex2g  25132  prltub  25260  tolat  25286  latdir  25295  svli2  25484  lemindclsbu  25995  indcls2  25996  upixp  26403  caushft  26477  sstotbnd3  26500  totbndss  26501  unichnidl  26656  ispridl2  26663  elrfirn2  26771  mzpsubst  26826  eluzrabdioph  26887
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator