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

Theorem ralimdv 2787
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 2786 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   A.wral 2707
This theorem is referenced by:  poss  4508  sess1  4553  sess2  4554  tfindsg  4843  riinint  5129  iinpreima  5863  dffo4  5888  dffo5  5889  isoini2  6062  abianfp  6719  iiner  6979  xpf1o  7272  dffi3  7439  brwdom3  7553  xpwdomg  7556  bndrank  7770  cfub  8134  cff1  8143  cfflb  8144  cfslb2n  8153  cofsmo  8154  cfcoflem  8157  pwcfsdom  8463  fpwwe2lem13  8522  inawinalem  8569  grupr  8677  fsequb  11319  cau3lem  12163  caubnd2  12166  caubnd  12167  rlim2lt  12296  rlim3  12297  climshftlem  12373  isercolllem1  12463  climcau  12469  caucvgb  12478  serf0  12479  cvgcmp  12600  mreriincl  13828  acsfn1c  13892  islss4  16043  riinopn  16986  fiinbas  17022  baspartn  17024  isclo2  17157  lmcls  17371  lmcnp  17373  isnrm3  17428  1stcelcls  17529  llyss  17547  nllyss  17548  ptpjpre1  17608  txlly  17673  txnlly  17674  tx1stc  17687  xkococnlem  17696  fbunfip  17906  filssufilg  17948  cnpflf2  18037  fcfnei  18072  isucn2  18314  rescncf  18932  lebnum  18994  cfilss  19228  fgcfil  19229  iscau4  19237  cmetcaulem  19246  cfilres  19254  caussi  19255  ovolunlem1  19398  ulmclm  20308  ulmcaulem  20315  ulmcau  20316  ulmss  20318  rlimcnp  20809  cxploglim  20821  lgsdchr  21137  pntlemp  21309  nmlnoubi  22302  lnon0  22304  disjpreima  24031  resspos  24192  resstos  24193  iccllyscon  24942  cvmlift2lem1  24994  setlikess  25475  axcontlem4  25911  upixp  26445  caushft  26481  sstotbnd3  26499  totbndss  26500  unichnidl  26655  ispridl2  26662  elrfirn2  26764  mzpsubst  26819  eluzrabdioph  26880  cshwssizelem1a  28313  usg2wlkeq  28342  3cyclfrgrarn2  28478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712
  Copyright terms: Public domain W3C validator