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  5713  dffo5  5714  isoini2  5869  rdgivallem  6448  iinerm  6675  xpf1o  6914  exmidontriimlem3  7306  exmidontriim  7308  resqrexlemgt0  11202  cau3lem  11296  caubnd2  11299  climshftlemg  11484  climcau  11529  climcaucn  11533  serf0  11534  modfsummodlemstep  11639  bezoutlemmain  12190  ctinf  12672  strsetsid  12736  imasaddfnlemg  13016  islss4  14014  fiinbas  14369  baspartn  14370  lmtopcnp  14570  rescncf  14901  limcresi  14986