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  4389  sess1  4428  sess2  4429  riinint  4985  dffo4  5785  dffo5  5786  isoini2  5949  rdgivallem  6533  iinerm  6762  xpf1o  7013  exmidontriimlem3  7416  exmidontriim  7418  resqrexlemgt0  11546  cau3lem  11640  caubnd2  11643  climshftlemg  11828  climcau  11873  climcaucn  11877  serf0  11878  modfsummodlemstep  11983  bezoutlemmain  12534  ctinf  13016  strsetsid  13080  imasaddfnlemg  13362  islss4  14361  fiinbas  14738  baspartn  14739  lmtopcnp  14939  rescncf  15270  limcresi  15355  upgrwlkedg  16102  uspgr2wlkeq  16106  umgrwlknloop  16109