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

Theorem ralimdv 2593
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 2592 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 2516
This theorem is referenced by:  poss  4253  sess1  4298  sess2  4299  tfindsg  4588  riinint  4888  iinpreima  5554  dffo4  5575  dffo5  5576  isoini2  5735  abianfp  6404  iiner  6664  xpf1o  6956  dffi3  7117  brwdom3  7229  xpwdomg  7232  bndrank  7446  cfub  7808  cff1  7817  cfflb  7818  cfslb2n  7827  cofsmo  7828  cfcoflem  7831  pwcfsdom  8138  fpwwe2lem13  8197  inawinalem  8244  grupr  8352  fsequb  10968  cau3lem  11768  caubnd2  11771  caubnd  11772  rlim2lt  11901  rlim3  11902  climshftlem  11978  isercolllem1  12068  climcau  12074  caucvgb  12082  serf0  12083  cvgcmp  12204  mreriincl  13427  acsfn1c  13491  islss4  15646  riinopn  16581  fiinbas  16617  baspartn  16619  isclo2  16752  lmcls  16957  lmcnp  16959  isnrm3  17014  1stcelcls  17114  llyss  17132  nllyss  17133  ptpjpre1  17193  txlly  17257  txnlly  17258  tx1stc  17271  xkococnlem  17280  fbunfip  17491  filssufilg  17533  cnpflf2  17622  fcfnei  17657  rescncf  18328  lebnum  18389  cfilss  18623  fgcfil  18624  iscau4  18632  cmetcaulem  18641  cfilres  18649  caussi  18650  ovolunlem1  18783  ulmclm  19693  ulmcaulem  19698  ulmcau  19699  ulmss  19701  rlimcnp  20187  cxploglim  20199  lgsdchr  20514  pntlemp  20686  nmlnoubi  21299  lnon0  21301  iccllyscon  23118  cvmlift2lem1  23170  setlikess  23529  axcontlem4  23935  ab2rexex2g  24464  prltub  24592  tolat  24618  latdir  24627  svli2  24816  lemindclsbu  25327  indcls2  25328  upixp  25735  caushft  25809  sstotbnd3  25832  totbndss  25833  unichnidl  25988  ispridl2  25995  elrfirn2  26103  mzpsubst  26158  eluzrabdioph  26219
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 2520
  Copyright terms: Public domain W3C validator