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

Theorem ralimdv 2730
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 452 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32ralimdva 2729 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   A.wral 2651
This theorem is referenced by:  poss  4448  sess1  4493  sess2  4494  tfindsg  4782  riinint  5068  iinpreima  5801  dffo4  5826  dffo5  5827  isoini2  6000  abianfp  6654  iiner  6914  xpf1o  7207  dffi3  7373  brwdom3  7485  xpwdomg  7488  bndrank  7702  cfub  8064  cff1  8073  cfflb  8074  cfslb2n  8083  cofsmo  8084  cfcoflem  8087  pwcfsdom  8393  fpwwe2lem13  8452  inawinalem  8499  grupr  8607  fsequb  11243  cau3lem  12087  caubnd2  12090  caubnd  12091  rlim2lt  12220  rlim3  12221  climshftlem  12297  isercolllem1  12387  climcau  12393  caucvgb  12402  serf0  12403  cvgcmp  12524  mreriincl  13752  acsfn1c  13816  islss4  15967  riinopn  16906  fiinbas  16942  baspartn  16944  isclo2  17077  lmcls  17290  lmcnp  17292  isnrm3  17347  1stcelcls  17447  llyss  17465  nllyss  17466  ptpjpre1  17526  txlly  17591  txnlly  17592  tx1stc  17605  xkococnlem  17614  fbunfip  17824  filssufilg  17866  cnpflf2  17955  fcfnei  17990  isucn2  18232  rescncf  18800  lebnum  18862  cfilss  19096  fgcfil  19097  iscau4  19105  cmetcaulem  19114  cfilres  19122  caussi  19123  ovolunlem1  19262  ulmclm  20172  ulmcaulem  20179  ulmcau  20180  ulmss  20182  rlimcnp  20673  cxploglim  20685  lgsdchr  21001  pntlemp  21173  nmlnoubi  22147  lnon0  22149  disjpreima  23872  resspos  24028  resstos  24029  iccllyscon  24718  cvmlift2lem1  24770  setlikess  25221  axcontlem4  25622  upixp  26124  caushft  26160  sstotbnd3  26178  totbndss  26179  unichnidl  26334  ispridl2  26341  elrfirn2  26443  mzpsubst  26498  eluzrabdioph  26559  3cyclfrgrarn2  27769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2656
  Copyright terms: Public domain W3C validator