Theorem ralimdv 2806

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

Syntax hints:   -> wi 4   e. wcel 1904   A.wral 2756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-an 378  df-ral 2761

This theorem is referenced by:  poss  4762  sess1  4807  sess2  4808  riinint  5097  iinpreima  6025  dffo4  6053  dffo5  6054  isoini2  6248  tfindsg  6706  iiner  7453  xpf1o  7752  dffi3  7963  brwdom3  8115  xpwdomg  8118  bndrank  8330  cfub  8697  cff1  8706  cfflb  8707  cfslb2n  8716  cofsmo  8717  cfcoflem  8720  pwcfsdom  9026  fpwwe2lem13  9085  inawinalem  9132  grupr  9240  fsequb  12226  cau3lem  13494  caubnd2  13497  caubnd  13498  rlim2lt  13638  rlim3  13639  climshftlem  13715  isercolllem1  13805  climcau  13811  caucvgb  13823  serf0  13824  modfsummods  13930  cvgcmp  13953  mreriincl  15582  acsfn1c  15646  islss4  18263  riinopn  20015  fiinbas  20044  baspartn  20046  isclo2  20181  lmcls  20395  lmcnp  20397  isnrm3  20452  1stcelcls  20553  llyss  20571  nllyss  20572  ptpjpre1  20663  txlly  20728  txnlly  20729  tx1stc  20742  xkococnlem  20751  fbunfip  20962  filssufilg  21004  cnpflf2  21093  fcfnei  21128  isucn2  21372  rescncf  22007  lebnum  22073  cfilss  22318  fgcfil  22319  iscau4  22327  cmetcaulem  22336  cfilres  22344  caussi  22345  ovolunlem1  22528  ulmclm  23421  ulmcaulem  23428  ulmcau  23429  ulmss  23431  rlimcnp  23970  cxploglim  23982  lgsdchr  24355  pntlemp  24527  axcontlem4  25076  usg2wlkeq  25515  3cyclfrgrarn2  25821  nmlnoubi  26518  lnon0  26520  disjpreima  28271  resspos  28495  resstos  28496  submarchi  28577  crefss  28750  iccllyscon  30045  cvmlift2lem1  30097  ss2mcls  30278  mclsax  30279  poimirlem25  32029  poimirlem27  32031  upixp  32120  caushft  32154  sstotbnd3  32172  totbndss  32173  unichnidl  32328  ispridl2  32335  elrfirn2  35609  mzpsubst  35661  eluzrabdioph  35720  fourierdlem103  38185  fourierdlem104  38186  qndenserrnbllem  38275  ralralimp  39134  ewlkle  39811  umgr1wlknloop  39848