Theorem ralimdva 2537

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 1521	. 2 ⊢ Ⅎ𝑥𝜑
2		ralimdva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	1, 2	ralimdaa 2536	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  ralimdv  2538  ralimdvva  2539  f1mpt  5750  isores3  5794  caofrss  6085  caoftrn  6086  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  tfrcl  6343  exmidomniim  7117  exmidontri2or  7220  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  indstr  9552  caucvgre  10945  rexuz3  10954  resqrexlemgt0  10984  resqrexlemglsq  10986  cau3lem  11078  rexanre  11184  rexico  11185  2clim  11264  climcn1  11271  climcn2  11272  subcn2  11274  climsqz  11298  climsqz2  11299  climcvg1nlem  11312  fprodsplitdc  11559  bezoutlemaz  11958  bezoutlembz  11959  bezoutlembi  11960  pcfac  12302  pockthg  12309  infpnlem1  12311  isgrpinv  12756  cncnp  13024  txlm  13073  metequiv2  13290  metcnpi3  13311  rescncf  13362  cncfco  13372  suplociccreex  13396  limcresi  13429  cnplimcim  13430  cnplimclemr  13432  cnlimcim  13434  limccnpcntop  13438  limccoap  13441  2sqlem6  13750  bj-charfunbi  13846  nninffeq  14053  tridceq  14088