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

Theorem ralimdv 2597
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 2596 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   A.wral 2518
This theorem is referenced by:  poss  4288  sess1  4333  sess2  4334  tfindsg  4623  riinint  4923  iinpreima  5589  dffo4  5610  dffo5  5611  isoini2  5770  abianfp  6439  iiner  6699  xpf1o  6991  dffi3  7152  brwdom3  7264  xpwdomg  7267  bndrank  7481  cfub  7843  cff1  7852  cfflb  7853  cfslb2n  7862  cofsmo  7863  cfcoflem  7866  pwcfsdom  8173  fpwwe2lem13  8232  inawinalem  8279  grupr  8387  fsequb  11003  cau3lem  11803  caubnd2  11806  caubnd  11807  rlim2lt  11936  rlim3  11937  climshftlem  12013  isercolllem1  12103  climcau  12109  caucvgb  12117  serf0  12118  cvgcmp  12239  mreriincl  13462  acsfn1c  13526  islss4  15681  riinopn  16616  fiinbas  16652  baspartn  16654  isclo2  16787  lmcls  16992  lmcnp  16994  isnrm3  17049  1stcelcls  17149  llyss  17167  nllyss  17168  ptpjpre1  17228  txlly  17292  txnlly  17293  tx1stc  17306  xkococnlem  17315  fbunfip  17526  filssufilg  17568  cnpflf2  17657  fcfnei  17692  rescncf  18363  lebnum  18424  cfilss  18658  fgcfil  18659  iscau4  18667  cmetcaulem  18676  cfilres  18684  caussi  18685  ovolunlem1  18818  ulmclm  19728  ulmcaulem  19733  ulmcau  19734  ulmss  19736  rlimcnp  20222  cxploglim  20234  lgsdchr  20549  pntlemp  20721  nmlnoubi  21334  lnon0  21336  iccllyscon  23153  cvmlift2lem1  23205  setlikess  23564  axcontlem4  23970  ab2rexex2g  24499  prltub  24627  tolat  24653  latdir  24662  svli2  24851  lemindclsbu  25362  indcls2  25363  upixp  25770  caushft  25844  sstotbnd3  25867  totbndss  25868  unichnidl  26023  ispridl2  26030  elrfirn2  26138  mzpsubst  26193  eluzrabdioph  26254
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-nf 1540  df-ral 2523
  Copyright terms: Public domain W3C validator