Theorem ralimdv 3147

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1810). (Contributed by NM, 8-Oct-2003.)

Hypothesis

Ref	Expression
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 3145	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  r19.21v  3158  ralimdvv  3186  ss2ralv  4017  poss  5548  sess1  5603  sess2  5604  riinint  5935  iinpreima  7041  dffo4  7075  dffo5  7076  isoini2  7314  tfindsg  7837  el2mpocsbcl  8064  xpord3inddlem  8133  iiner  8762  xpf1o  9103  dffi3  9382  brwdom3  9535  xpwdomg  9538  ttrclss  9673  bndrank  9794  cfub  10202  cff1  10211  cfflb  10212  cfslb2n  10221  cofsmo  10222  cfcoflem  10225  pwcfsdom  10536  fpwwe2lem12  10595  inawinalem  10642  grupr  10750  fsequb  13940  cau3lem  15321  caubnd2  15324  caubnd  15325  rlim2lt  15463  rlim3  15464  climshftlem  15540  climcau  15637  caucvgb  15646  serf0  15647  modfsummods  15759  cvgcmp  15782  mreriincl  17559  acsfn1c  17623  islss4  20868  riinopn  22795  fiinbas  22839  baspartn  22841  isclo2  22975  lmcls  23189  lmcnp  23191  isnrm3  23246  1stcelcls  23348  llyss  23366  nllyss  23367  ptpjpre1  23458  txlly  23523  txnlly  23524  tx1stc  23537  xkococnlem  23546  fbunfip  23756  filssufilg  23798  cnpflf2  23887  fcfnei  23922  isucn2  24166  rescncf  24790  lebnum  24863  cfilss  25170  fgcfil  25171  iscau4  25179  cmetcaulem  25188  caussi  25197  ovolunlem1  25398  ulmclm  26296  ulmcaulem  26303  ulmcau  26304  ulmss  26306  rlimcnp  26875  cxploglim  26888  2sqreunnlem2  27366  pntlemp  27521  nosupno  27615  nosupres  27619  noinfno  27630  noinfres  27634  sssslt2  27708  madebdayim  27799  madebdaylemold  27809  axcontlem4  28894  ewlkle  29533  uspgr2wlkeq  29574  umgrwlknloop  29577  wlkiswwlksupgr2  29807  3cyclfrgrrn2  30216  nmlnoubi  30725  lnon0  30727  disjpreima  32513  resspos  32892  resstos  32893  submarchi  33140  prmidl2  33412  crefss  33839  iccllysconn  35237  cvmlift2lem1  35289  dmopab3rexdif  35392  ss2mcls  35555  mclsax  35556  isinf2  37393  poimirlem25  37639  poimirlem27  37641  upixp  37723  caushft  37755  sstotbnd3  37770  totbndss  37771  unichnidl  38025  ispridl2  38032  elrfirn2  42684  mzpsubst  42736  eluzrabdioph  42794  neik0pk1imk0  44036  mnuop3d  44260  ismnushort  44290  pwclaxpow  44974  limsupub  45702  limsupre3lem  45730  climuzlem  45741  xlimbr  45825  fourierdlem103  46207  fourierdlem104  46208  qndenserrnbllem  46292  2reuimp  47116  ralralimp  47279