Theorem ralimdv 2503

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 274	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 2502	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 1481  ∀wral 2417

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  poss  4228  sess1  4267  sess2  4268  riinint  4808  dffo4  5576  dffo5  5577  isoini2  5728  rdgivallem  6286  iinerm  6509  xpf1o  6746  resqrexlemgt0  10824  cau3lem  10918  caubnd2  10921  climshftlemg  11103  climcau  11148  climcaucn  11152  serf0  11153  modfsummodlemstep  11258  bezoutlemmain  11722  ctinf  11979  strsetsid  12031  fiinbas  12255  baspartn  12256  lmtopcnp  12458  rescncf  12776  limcresi  12843