Theorem ralimdv 2842

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1679). (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 466	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	ralimdva 2840	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1870   A.wral 2782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751

This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2787

This theorem is referenced by:  poss  4777  sess1  4822  sess2  4823  riinint  5111  iinpreima  6025  dffo4  6053  dffo5  6054  isoini2  6245  tfindsg  6701  iiner  7443  xpf1o  7740  dffi3  7951  brwdom3  8097  xpwdomg  8100  bndrank  8311  cfub  8677  cff1  8686  cfflb  8687  cfslb2n  8696  cofsmo  8697  cfcoflem  8700  pwcfsdom  9006  fpwwe2lem13  9066  inawinalem  9113  grupr  9221  fsequb  12185  cau3lem  13396  caubnd2  13399  caubnd  13400  rlim2lt  13539  rlim3  13540  climshftlem  13616  isercolllem1  13706  climcau  13712  caucvgb  13724  serf0  13725  modfsummods  13831  cvgcmp  13854  mreriincl  15455  acsfn1c  15519  islss4  18120  riinopn  19869  fiinbas  19898  baspartn  19900  isclo2  20035  lmcls  20249  lmcnp  20251  isnrm3  20306  1stcelcls  20407  llyss  20425  nllyss  20426  ptpjpre1  20517  txlly  20582  txnlly  20583  tx1stc  20596  xkococnlem  20605  fbunfip  20815  filssufilg  20857  cnpflf2  20946  fcfnei  20981  isucn2  21225  rescncf  21825  lebnum  21888  cfilss  22133  fgcfil  22134  iscau4  22142  cmetcaulem  22151  cfilres  22159  caussi  22160  ovolunlem1  22328  ulmclm  23207  ulmcaulem  23214  ulmcau  23215  ulmss  23217  rlimcnp  23756  cxploglim  23768  lgsdchr  24139  pntlemp  24311  axcontlem4  24843  usg2wlkeq  25281  3cyclfrgrarn2  25587  nmlnoubi  26282  lnon0  26284  disjpreima  28033  resspos  28258  resstos  28259  submarchi  28341  crefss  28515  iccllyscon  29761  cvmlift2lem1  29813  ss2mcls  29994  mclsax  29995  poimirlem25  31669  poimirlem27  31671  upixp  31760  caushft  31794  sstotbnd3  31812  totbndss  31813  unichnidl  31968  ispridl2  31975  elrfirn2  35247  mzpsubst  35299  eluzrabdioph  35358  fourierdlem103  37641  fourierdlem104  37642  ralralimp  38372