Theorem ralimdv 2745

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

Syntax hints:   -> wi 4   e. wcel 1721   A.wral 2666

This theorem is referenced by:  poss  4465  sess1  4510  sess2  4511  tfindsg  4799  riinint  5085  iinpreima  5819  dffo4  5844  dffo5  5845  isoini2  6018  abianfp  6675  iiner  6935  xpf1o  7228  dffi3  7394  brwdom3  7506  xpwdomg  7509  bndrank  7723  cfub  8085  cff1  8094  cfflb  8095  cfslb2n  8104  cofsmo  8105  cfcoflem  8108  pwcfsdom  8414  fpwwe2lem13  8473  inawinalem  8520  grupr  8628  fsequb  11269  cau3lem  12113  caubnd2  12116  caubnd  12117  rlim2lt  12246  rlim3  12247  climshftlem  12323  isercolllem1  12413  climcau  12419  caucvgb  12428  serf0  12429  cvgcmp  12550  mreriincl  13778  acsfn1c  13842  islss4  15993  riinopn  16936  fiinbas  16972  baspartn  16974  isclo2  17107  lmcls  17320  lmcnp  17322  isnrm3  17377  1stcelcls  17477  llyss  17495  nllyss  17496  ptpjpre1  17556  txlly  17621  txnlly  17622  tx1stc  17635  xkococnlem  17644  fbunfip  17854  filssufilg  17896  cnpflf2  17985  fcfnei  18020  isucn2  18262  rescncf  18880  lebnum  18942  cfilss  19176  fgcfil  19177  iscau4  19185  cmetcaulem  19194  cfilres  19202  caussi  19203  ovolunlem1  19346  ulmclm  20256  ulmcaulem  20263  ulmcau  20264  ulmss  20266  rlimcnp  20757  cxploglim  20769  lgsdchr  21085  pntlemp  21257  nmlnoubi  22250  lnon0  22252  disjpreima  23979  resspos  24140  resstos  24141  iccllyscon  24890  cvmlift2lem1  24942  setlikess  25409  axcontlem4  25810  upixp  26321  caushft  26357  sstotbnd3  26375  totbndss  26376  unichnidl  26531  ispridl2  26538  elrfirn2  26640  mzpsubst  26695  eluzrabdioph  26756  3cyclfrgrarn2  28118

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671