Theorem ralimdv 2797

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1682). (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

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	adantr 467	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	ralimdva 2795	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1886   A.wral 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757

This theorem depends on definitions:  df-bi 189  df-an 373  df-ral 2741

This theorem is referenced by:  poss  4756  sess1  4801  sess2  4802  riinint  5090  iinpreima  6008  dffo4  6036  dffo5  6037  isoini2  6228  tfindsg  6684  iiner  7432  xpf1o  7731  dffi3  7942  brwdom3  8094  xpwdomg  8097  bndrank  8309  cfub  8676  cff1  8685  cfflb  8686  cfslb2n  8695  cofsmo  8696  cfcoflem  8699  pwcfsdom  9005  fpwwe2lem13  9064  inawinalem  9111  grupr  9219  fsequb  12185  cau3lem  13410  caubnd2  13413  caubnd  13414  rlim2lt  13554  rlim3  13555  climshftlem  13631  isercolllem1  13721  climcau  13727  caucvgb  13739  serf0  13740  modfsummods  13846  cvgcmp  13869  mreriincl  15497  acsfn1c  15561  islss4  18178  riinopn  19931  fiinbas  19960  baspartn  19962  isclo2  20097  lmcls  20311  lmcnp  20313  isnrm3  20368  1stcelcls  20469  llyss  20487  nllyss  20488  ptpjpre1  20579  txlly  20644  txnlly  20645  tx1stc  20658  xkococnlem  20667  fbunfip  20877  filssufilg  20919  cnpflf2  21008  fcfnei  21043  isucn2  21287  rescncf  21922  lebnum  21988  cfilss  22233  fgcfil  22234  iscau4  22242  cmetcaulem  22251  cfilres  22259  caussi  22260  ovolunlem1  22443  ulmclm  23335  ulmcaulem  23342  ulmcau  23343  ulmss  23345  rlimcnp  23884  cxploglim  23896  lgsdchr  24269  pntlemp  24441  axcontlem4  24990  usg2wlkeq  25429  3cyclfrgrarn2  25735  nmlnoubi  26430  lnon0  26432  disjpreima  28187  resspos  28413  resstos  28414  submarchi  28496  crefss  28669  iccllyscon  29966  cvmlift2lem1  30018  ss2mcls  30199  mclsax  30200  poimirlem25  31958  poimirlem27  31960  upixp  32049  caushft  32083  sstotbnd3  32101  totbndss  32102  unichnidl  32257  ispridl2  32264  elrfirn2  35532  mzpsubst  35584  eluzrabdioph  35643  fourierdlem103  38067  fourierdlem104  38068  qndenserrnbllem  38157  ralralimp  38981  ewlkle  39606  umgr1wlknloop  39638