Theorem ralimdv 2573

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)

Hypothesis

Ref	Expression
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 2572	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2175  ∀wral 2483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488

This theorem is referenced by:  poss  4344  sess1  4383  sess2  4384  riinint  4938  dffo4  5727  dffo5  5728  isoini2  5887  rdgivallem  6466  iinerm  6693  xpf1o  6940  exmidontriimlem3  7334  exmidontriim  7336  resqrexlemgt0  11302  cau3lem  11396  caubnd2  11399  climshftlemg  11584  climcau  11629  climcaucn  11633  serf0  11634  modfsummodlemstep  11739  bezoutlemmain  12290  ctinf  12772  strsetsid  12836  imasaddfnlemg  13117  islss4  14115  fiinbas  14492  baspartn  14493  lmtopcnp  14693  rescncf  15024  limcresi  15109