Theorem ralimdv 2874

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 2872	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1767   A.wral 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819

This theorem is referenced by:  poss  4802  sess1  4847  sess2  4848  riinint  5259  iinpreima  6011  dffo4  6037  dffo5  6038  isoini2  6223  tfindsg  6679  iiner  7383  xpf1o  7679  dffi3  7891  brwdom3  8008  xpwdomg  8011  bndrank  8259  cfub  8629  cff1  8638  cfflb  8639  cfslb2n  8648  cofsmo  8649  cfcoflem  8652  pwcfsdom  8958  fpwwe2lem13  9020  inawinalem  9067  grupr  9175  fsequb  12053  cau3lem  13150  caubnd2  13153  caubnd  13154  rlim2lt  13283  rlim3  13284  climshftlem  13360  isercolllem1  13450  climcau  13456  caucvgb  13465  serf0  13466  modfsummods  13570  cvgcmp  13593  mreriincl  14853  acsfn1c  14917  islss4  17408  riinopn  19212  fiinbas  19248  baspartn  19250  isclo2  19383  lmcls  19597  lmcnp  19599  isnrm3  19654  1stcelcls  19756  llyss  19774  nllyss  19775  ptpjpre1  19835  txlly  19900  txnlly  19901  tx1stc  19914  xkococnlem  19923  fbunfip  20133  filssufilg  20175  cnpflf2  20264  fcfnei  20299  isucn2  20545  rescncf  21164  lebnum  21227  cfilss  21472  fgcfil  21473  iscau4  21481  cmetcaulem  21490  cfilres  21498  caussi  21499  ovolunlem1  21671  ulmclm  22544  ulmcaulem  22551  ulmcau  22552  ulmss  22554  rlimcnp  23051  cxploglim  23063  lgsdchr  23379  pntlemp  23551  axcontlem4  23974  usg2wlkeq  24412  3cyclfrgrarn2  24718  nmlnoubi  25415  lnon0  25417  disjpreima  27146  resspos  27337  resstos  27338  submarchi  27420  iccllyscon  28363  cvmlift2lem1  28415  setlikess  28880  upixp  29851  caushft  29885  sstotbnd3  29903  totbndss  29904  unichnidl  30059  ispridl2  30066  elrfirn2  30260  mzpsubst  30313  eluzrabdioph  30371  fourierdlem103  31538  fourierdlem104  31539  ralralimp  31790  mndmgm  31955