Theorem ralimdva 2497

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 2496	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

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

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 2419

This theorem is referenced by:  ralimdv  2498  ralimdvva  2499  f1mpt  5665  isores3  5709  caofrss  5999  caoftrn  6000  tfrlemibxssdm  6217  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  tfrcl  6254  exmidomniim  7006  caucvgsrlemoffcau  7599  caucvgsrlemoffres  7601  indstr  9381  caucvgre  10746  rexuz3  10755  resqrexlemgt0  10785  resqrexlemglsq  10787  cau3lem  10879  rexanre  10985  rexico  10986  2clim  11063  climcn1  11070  climcn2  11071  subcn2  11073  climsqz  11097  climsqz2  11098  climcvg1nlem  11111  bezoutlemaz  11680  bezoutlembz  11681  bezoutlembi  11682  cncnp  12388  txlm  12437  metequiv2  12654  metcnpi3  12675  rescncf  12726  cncfco  12736  suplociccreex  12760  limcresi  12793  cnplimcim  12794  cnplimclemr  12796  cnlimcim  12798  limccnpcntop  12802  limccoap  12805  nninffeq  13205