Theorem ralimdv 2598

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  poss  4388  sess1  4427  sess2  4428  riinint  4984  dffo4  5782  dffo5  5783  isoini2  5942  rdgivallem  6525  iinerm  6752  xpf1o  7001  exmidontriimlem3  7401  exmidontriim  7403  resqrexlemgt0  11526  cau3lem  11620  caubnd2  11623  climshftlemg  11808  climcau  11853  climcaucn  11857  serf0  11858  modfsummodlemstep  11963  bezoutlemmain  12514  ctinf  12996  strsetsid  13060  imasaddfnlemg  13342  islss4  14340  fiinbas  14717  baspartn  14718  lmtopcnp  14918  rescncf  15249  limcresi  15334