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

Theorem ralimdv 2635
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 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32ralimdva 2634 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   A.wral 2556
This theorem is referenced by:  poss  4332  sess1  4377  sess2  4378  tfindsg  4667  riinint  4951  iinpreima  5671  dffo4  5692  dffo5  5693  isoini2  5852  abianfp  6487  iiner  6747  xpf1o  7039  dffi3  7200  brwdom3  7312  xpwdomg  7315  bndrank  7529  cfub  7891  cff1  7900  cfflb  7901  cfslb2n  7910  cofsmo  7911  cfcoflem  7914  pwcfsdom  8221  fpwwe2lem13  8280  inawinalem  8327  grupr  8435  fsequb  11053  cau3lem  11854  caubnd2  11857  caubnd  11858  rlim2lt  11987  rlim3  11988  climshftlem  12064  isercolllem1  12154  climcau  12160  caucvgb  12168  serf0  12169  cvgcmp  12290  mreriincl  13516  acsfn1c  13580  islss4  15735  riinopn  16670  fiinbas  16706  baspartn  16708  isclo2  16841  lmcls  17046  lmcnp  17048  isnrm3  17103  1stcelcls  17203  llyss  17221  nllyss  17222  ptpjpre1  17282  txlly  17346  txnlly  17347  tx1stc  17360  xkococnlem  17369  fbunfip  17580  filssufilg  17622  cnpflf2  17711  fcfnei  17746  rescncf  18417  lebnum  18478  cfilss  18712  fgcfil  18713  iscau4  18721  cmetcaulem  18730  cfilres  18738  caussi  18739  ovolunlem1  18872  ulmclm  19782  ulmcaulem  19787  ulmcau  19788  ulmss  19790  rlimcnp  20276  cxploglim  20288  lgsdchr  20603  pntlemp  20775  nmlnoubi  21390  lnon0  21392  disjpreima  23376  iccllyscon  23796  cvmlift2lem1  23848  setlikess  24266  axcontlem4  24667  ab2rexex2g  25235  prltub  25363  tolat  25389  latdir  25398  svli2  25587  lemindclsbu  26098  indcls2  26099  upixp  26506  caushft  26580  sstotbnd3  26603  totbndss  26604  unichnidl  26759  ispridl2  26766  elrfirn2  26874  mzpsubst  26929  eluzrabdioph  26990
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator