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

Theorem ralimdv 2584
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 2583 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 2509
This theorem is referenced by:  poss  4209  sess1  4254  sess2  4255  tfindsg  4542  riinint  4842  iinpreima  5507  dffo4  5528  dffo5  5529  isoini2  5688  abianfp  6357  iiner  6617  xpf1o  6908  dffi3  7068  brwdom3  7180  xpwdomg  7183  bndrank  7397  cfub  7759  cff1  7768  cfflb  7769  cfslb2n  7778  cofsmo  7779  cfcoflem  7782  pwcfsdom  8085  fpwwe2lem13  8144  inawinalem  8191  grupr  8299  fsequb  10915  cau3lem  11715  caubnd2  11718  caubnd  11719  rlim2lt  11848  rlim3  11849  climshftlem  11925  isercolllem1  12015  climcau  12021  caucvgb  12029  serf0  12030  cvgcmp  12151  mreriincl  13372  acsfn1c  13408  islss4  15554  riinopn  16486  fiinbas  16522  baspartn  16524  isclo2  16657  lmcls  16862  lmcnp  16864  isnrm3  16919  1stcelcls  17019  llyss  17037  nllyss  17038  ptpjpre1  17098  txlly  17162  txnlly  17163  tx1stc  17176  xkococnlem  17185  fbunfip  17396  filssufilg  17438  cnpflf2  17527  fcfnei  17562  rescncf  18233  lebnum  18294  cfilss  18528  fgcfil  18529  iscau4  18537  cmetcaulem  18546  cfilres  18554  caussi  18555  ovolunlem1  18688  ulmclm  19598  ulmcaulem  19603  ulmcau  19604  ulmss  19606  rlimcnp  20092  cxploglim  20104  lgsdchr  20419  pntlemp  20591  nmlnoubi  21204  lnon0  21206  iccllyscon  22952  cvmlift2lem1  23004  setlikess  23363  axcontlem4  23769  ab2rexex2g  24298  prltub  24426  tolat  24452  latdir  24461  svli2  24650  lemindclsbu  25161  indcls2  25162  upixp  25569  caushft  25643  sstotbnd3  25666  totbndss  25667  unichnidl  25822  ispridl2  25829  elrfirn2  25937  mzpsubst  25992  eluzrabdioph  26053
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 2513
  Copyright terms: Public domain W3C validator