Theorem ralimdv 2794

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 465	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	ralimdva 2793	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1756   A.wral 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

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

This theorem is referenced by:  poss  4642  sess1  4687  sess2  4688  riinint  5095  iinpreima  5832  dffo4  5858  dffo5  5859  isoini2  6029  tfindsg  6470  iiner  7171  xpf1o  7472  dffi3  7680  brwdom3  7796  xpwdomg  7799  bndrank  8047  cfub  8417  cff1  8426  cfflb  8427  cfslb2n  8436  cofsmo  8437  cfcoflem  8440  pwcfsdom  8746  fpwwe2lem13  8808  inawinalem  8855  grupr  8963  fsequb  11796  cau3lem  12841  caubnd2  12844  caubnd  12845  rlim2lt  12974  rlim3  12975  climshftlem  13051  isercolllem1  13141  climcau  13147  caucvgb  13156  serf0  13157  cvgcmp  13278  mreriincl  14535  acsfn1c  14599  islss4  17042  riinopn  18520  fiinbas  18556  baspartn  18558  isclo2  18691  lmcls  18905  lmcnp  18907  isnrm3  18962  1stcelcls  19064  llyss  19082  nllyss  19083  ptpjpre1  19143  txlly  19208  txnlly  19209  tx1stc  19222  xkococnlem  19231  fbunfip  19441  filssufilg  19483  cnpflf2  19572  fcfnei  19607  isucn2  19853  rescncf  20472  lebnum  20535  cfilss  20780  fgcfil  20781  iscau4  20789  cmetcaulem  20798  cfilres  20806  caussi  20807  ovolunlem1  20979  ulmclm  21851  ulmcaulem  21858  ulmcau  21859  ulmss  21861  rlimcnp  22358  cxploglim  22370  lgsdchr  22686  pntlemp  22858  axcontlem4  23212  nmlnoubi  24195  lnon0  24197  disjpreima  25927  resspos  26119  resstos  26120  submarchi  26202  iccllyscon  27138  cvmlift2lem1  27190  setlikess  27655  upixp  28621  caushft  28655  sstotbnd3  28673  totbndss  28674  unichnidl  28829  ispridl2  28836  elrfirn2  29030  mzpsubst  29083  eluzrabdioph  29142  ralralimp  30117  modfsummods  30242  usg2wlkeq  30287  3cyclfrgrarn2  30604