Theorem ralimdva 2531

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2135  ∀wral 2442

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-ral 2447

This theorem is referenced by:  ralimdv  2532  ralimdvva  2533  f1mpt  5733  isores3  5777  caofrss  6068  caoftrn  6069  tfrlemibxssdm  6286  tfr1onlembxssdm  6302  tfrcllembxssdm  6315  tfrcl  6323  exmidomniim  7096  exmidontri2or  7190  caucvgsrlemoffcau  7730  caucvgsrlemoffres  7732  indstr  9522  caucvgre  10909  rexuz3  10918  resqrexlemgt0  10948  resqrexlemglsq  10950  cau3lem  11042  rexanre  11148  rexico  11149  2clim  11228  climcn1  11235  climcn2  11236  subcn2  11238  climsqz  11262  climsqz2  11263  climcvg1nlem  11276  fprodsplitdc  11523  bezoutlemaz  11921  bezoutlembz  11922  bezoutlembi  11923  pcfac  12257  cncnp  12771  txlm  12820  metequiv2  13037  metcnpi3  13058  rescncf  13109  cncfco  13119  suplociccreex  13143  limcresi  13176  cnplimcim  13177  cnplimclemr  13179  cnlimcim  13181  limccnpcntop  13185  limccoap  13188  bj-charfunbi  13528  nninffeq  13734  tridceq  13769