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

Theorem ralimdv 2777
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 2776 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   A.wral 2697
This theorem is referenced by:  poss  4497  sess1  4542  sess2  4543  tfindsg  4832  riinint  5118  iinpreima  5852  dffo4  5877  dffo5  5878  isoini2  6051  abianfp  6708  iiner  6968  xpf1o  7261  dffi3  7428  brwdom3  7542  xpwdomg  7545  bndrank  7759  cfub  8121  cff1  8130  cfflb  8131  cfslb2n  8140  cofsmo  8141  cfcoflem  8144  pwcfsdom  8450  fpwwe2lem13  8509  inawinalem  8556  grupr  8664  fsequb  11306  cau3lem  12150  caubnd2  12153  caubnd  12154  rlim2lt  12283  rlim3  12284  climshftlem  12360  isercolllem1  12450  climcau  12456  caucvgb  12465  serf0  12466  cvgcmp  12587  mreriincl  13815  acsfn1c  13879  islss4  16030  riinopn  16973  fiinbas  17009  baspartn  17011  isclo2  17144  lmcls  17358  lmcnp  17360  isnrm3  17415  1stcelcls  17516  llyss  17534  nllyss  17535  ptpjpre1  17595  txlly  17660  txnlly  17661  tx1stc  17674  xkococnlem  17683  fbunfip  17893  filssufilg  17935  cnpflf2  18024  fcfnei  18059  isucn2  18301  rescncf  18919  lebnum  18981  cfilss  19215  fgcfil  19216  iscau4  19224  cmetcaulem  19233  cfilres  19241  caussi  19242  ovolunlem1  19385  ulmclm  20295  ulmcaulem  20302  ulmcau  20303  ulmss  20305  rlimcnp  20796  cxploglim  20808  lgsdchr  21124  pntlemp  21296  nmlnoubi  22289  lnon0  22291  disjpreima  24018  resspos  24179  resstos  24180  iccllyscon  24929  cvmlift2lem1  24981  setlikess  25462  axcontlem4  25898  upixp  26422  caushft  26458  sstotbnd3  26476  totbndss  26477  unichnidl  26632  ispridl2  26639  elrfirn2  26741  mzpsubst  26796  eluzrabdioph  26857  cshwssizelem1a  28242  3cyclfrgrarn2  28341
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator