Theorem ralimdva 2458

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1448  ∀wral 2375

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-ral 2380

This theorem is referenced by:  ralimdv  2459  ralimdvva  2460  f1mpt  5604  isores3  5648  caofrss  5937  caoftrn  5938  tfrlemibxssdm  6154  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  tfrcl  6191  exmidomniim  6925  caucvgsrlemoffcau  7493  caucvgsrlemoffres  7495  indstr  9238  caucvgre  10593  rexuz3  10602  resqrexlemgt0  10632  resqrexlemglsq  10634  cau3lem  10726  rexanre  10832  rexico  10833  2clim  10909  climcn1  10916  climcn2  10917  subcn2  10919  climsqz  10943  climsqz2  10944  climcvg1nlem  10957  bezoutlemaz  11484  bezoutlembz  11485  bezoutlembi  11486  cncnp  12180  txlm  12229  metequiv2  12424  metcnpi3  12441  rescncf  12481  cncfco  12491  limcresi  12515  cnplimcim  12516  cnlimcim  12517  limccnpcntop  12520  nninffeq  12800