Theorem ralimdva 2597

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
ralimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem ralimdva

Step	Hyp	Ref	Expression
1		nfv 1574	. 2 ⊢ Ⅎ𝑥𝜑
2		ralimdva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	1, 2	ralimdaa 2596	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∀wral 2508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralimdv  2598  ralimdvva  2599  f1mpt  5894  isores3  5938  caofrss  6248  caoftrn  6249  tfrlemibxssdm  6471  tfr1onlembxssdm  6487  tfrcllembxssdm  6500  tfrcl  6508  infidc  7097  exmidomniim  7304  exmidontri2or  7424  caucvgsrlemoffcau  7981  caucvgsrlemoffres  7983  indstr  9784  caucvgre  11487  rexuz3  11496  resqrexlemgt0  11526  resqrexlemglsq  11528  cau3lem  11620  rexanre  11726  rexico  11727  2clim  11807  climcn1  11814  climcn2  11815  subcn2  11817  climsqz  11841  climsqz2  11842  climcvg1nlem  11855  fprodsplitdc  12102  bezoutlemaz  12519  bezoutlembz  12520  bezoutlembi  12521  pcfac  12868  pockthg  12875  infpnlem1  12877  isgrpinv  13582  dfgrp3me  13628  issubg4m  13725  mplsubgfileminv  14658  cncnp  14898  txlm  14947  metequiv2  15164  metcnpi3  15185  rescncf  15249  cncfco  15259  suplociccreex  15292  limcresi  15334  cnplimcim  15335  cnplimclemr  15337  cnlimcim  15339  limccnpcntop  15343  limccoap  15346  2sqlem6  15793  wlkvtxiedgg  16042  bj-charfunbi  16132  nninffeq  16345  tridceq  16383