Theorem ralimdv 2785

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

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

Syntax hints:   -> wi 4   e. wcel 1755   A.wral 2705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710

This theorem is referenced by:  poss  4630  sess1  4675  sess2  4676  riinint  5083  iinpreima  5821  dffo4  5847  dffo5  5848  isoini2  6017  tfindsg  6460  abianfp  6900  iiner  7160  xpf1o  7461  dffi3  7669  brwdom3  7785  xpwdomg  7788  bndrank  8036  cfub  8406  cff1  8415  cfflb  8416  cfslb2n  8425  cofsmo  8426  cfcoflem  8429  pwcfsdom  8735  fpwwe2lem13  8796  inawinalem  8843  grupr  8951  fsequb  11780  cau3lem  12825  caubnd2  12828  caubnd  12829  rlim2lt  12958  rlim3  12959  climshftlem  13035  isercolllem1  13125  climcau  13131  caucvgb  13140  serf0  13141  cvgcmp  13261  mreriincl  14518  acsfn1c  14582  islss4  16964  riinopn  18362  fiinbas  18398  baspartn  18400  isclo2  18533  lmcls  18747  lmcnp  18749  isnrm3  18804  1stcelcls  18906  llyss  18924  nllyss  18925  ptpjpre1  18985  txlly  19050  txnlly  19051  tx1stc  19064  xkococnlem  19073  fbunfip  19283  filssufilg  19325  cnpflf2  19414  fcfnei  19449  isucn2  19695  rescncf  20314  lebnum  20377  cfilss  20622  fgcfil  20623  iscau4  20631  cmetcaulem  20640  cfilres  20648  caussi  20649  ovolunlem1  20821  ulmclm  21736  ulmcaulem  21743  ulmcau  21744  ulmss  21746  rlimcnp  22243  cxploglim  22255  lgsdchr  22571  pntlemp  22743  axcontlem4  23035  nmlnoubi  24018  lnon0  24020  disjpreima  25751  resspos  25942  resstos  25943  submarchi  26026  iccllyscon  26986  cvmlift2lem1  27038  setlikess  27502  upixp  28464  caushft  28498  sstotbnd3  28516  totbndss  28517  unichnidl  28672  ispridl2  28679  elrfirn2  28874  mzpsubst  28927  eluzrabdioph  28986  ralralimp  29962  modfsummods  30087  usg2wlkeq  30132  3cyclfrgrarn2  30449