Theorem ralimdva 2499

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  ∀wral 2416

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  ralimdv  2500  ralimdvva  2501  f1mpt  5672  isores3  5716  caofrss  6006  caoftrn  6007  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  tfrcl  6261  exmidomniim  7013  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  indstr  9388  caucvgre  10753  rexuz3  10762  resqrexlemgt0  10792  resqrexlemglsq  10794  cau3lem  10886  rexanre  10992  rexico  10993  2clim  11070  climcn1  11077  climcn2  11078  subcn2  11080  climsqz  11104  climsqz2  11105  climcvg1nlem  11118  bezoutlemaz  11691  bezoutlembz  11692  bezoutlembi  11693  cncnp  12399  txlm  12448  metequiv2  12665  metcnpi3  12686  rescncf  12737  cncfco  12747  suplociccreex  12771  limcresi  12804  cnplimcim  12805  cnplimclemr  12807  cnlimcim  12809  limccnpcntop  12813  limccoap  12816  nninffeq  13216