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

Theorem ralimdv 2749
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 2748 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   A.wral 2670
This theorem is referenced by:  poss  4469  sess1  4514  sess2  4515  tfindsg  4803  riinint  5089  iinpreima  5823  dffo4  5848  dffo5  5849  isoini2  6022  abianfp  6679  iiner  6939  xpf1o  7232  dffi3  7398  brwdom3  7510  xpwdomg  7513  bndrank  7727  cfub  8089  cff1  8098  cfflb  8099  cfslb2n  8108  cofsmo  8109  cfcoflem  8112  pwcfsdom  8418  fpwwe2lem13  8477  inawinalem  8524  grupr  8632  fsequb  11273  cau3lem  12117  caubnd2  12120  caubnd  12121  rlim2lt  12250  rlim3  12251  climshftlem  12327  isercolllem1  12417  climcau  12423  caucvgb  12432  serf0  12433  cvgcmp  12554  mreriincl  13782  acsfn1c  13846  islss4  15997  riinopn  16940  fiinbas  16976  baspartn  16978  isclo2  17111  lmcls  17324  lmcnp  17326  isnrm3  17381  1stcelcls  17481  llyss  17499  nllyss  17500  ptpjpre1  17560  txlly  17625  txnlly  17626  tx1stc  17639  xkococnlem  17648  fbunfip  17858  filssufilg  17900  cnpflf2  17989  fcfnei  18024  isucn2  18266  rescncf  18884  lebnum  18946  cfilss  19180  fgcfil  19181  iscau4  19189  cmetcaulem  19198  cfilres  19206  caussi  19207  ovolunlem1  19350  ulmclm  20260  ulmcaulem  20267  ulmcau  20268  ulmss  20270  rlimcnp  20761  cxploglim  20773  lgsdchr  21089  pntlemp  21261  nmlnoubi  22254  lnon0  22256  disjpreima  23983  resspos  24144  resstos  24145  iccllyscon  24894  cvmlift2lem1  24946  setlikess  25413  axcontlem4  25814  upixp  26325  caushft  26361  sstotbnd3  26379  totbndss  26380  unichnidl  26535  ispridl2  26542  elrfirn2  26644  mzpsubst  26699  eluzrabdioph  26760  3cyclfrgrarn2  28122
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 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2675
  Copyright terms: Public domain W3C validator