Theorem ralimdv 2565

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  poss  4334  sess1  4373  sess2  4374  riinint  4928  dffo4  5711  dffo5  5712  isoini2  5867  rdgivallem  6440  iinerm  6667  xpf1o  6906  exmidontriimlem3  7292  exmidontriim  7294  resqrexlemgt0  11187  cau3lem  11281  caubnd2  11284  climshftlemg  11469  climcau  11514  climcaucn  11518  serf0  11519  modfsummodlemstep  11624  bezoutlemmain  12175  ctinf  12657  strsetsid  12721  imasaddfnlemg  12967  islss4  13948  fiinbas  14295  baspartn  14296  lmtopcnp  14496  rescncf  14827  limcresi  14912