Theorem ralimdv 2601

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

Syntax hints:   → wi 4   ∈ wcel 2202  ∀wral 2511

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  poss  4401  sess1  4440  sess2  4441  riinint  4999  dffo4  5803  dffo5  5804  isoini2  5970  rdgivallem  6590  iinerm  6819  xpf1o  7073  exmidontriimlem3  7481  exmidontriim  7483  resqrexlemgt0  11643  cau3lem  11737  caubnd2  11740  climshftlemg  11925  climcau  11970  climcaucn  11974  serf0  11975  modfsummodlemstep  12081  bezoutlemmain  12632  ctinf  13114  strsetsid  13178  imasaddfnlemg  13460  islss4  14461  fiinbas  14843  baspartn  14844  lmtopcnp  15044  rescncf  15375  limcresi  15460  upgrwlkedg  16285  uspgr2wlkeq  16289  umgrwlknloop  16292