Theorem ralimdv 2574

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

Syntax hints:   → wi 4   ∈ wcel 2176  ∀wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  poss  4345  sess1  4384  sess2  4385  riinint  4939  dffo4  5728  dffo5  5729  isoini2  5888  rdgivallem  6467  iinerm  6694  xpf1o  6941  exmidontriimlem3  7335  exmidontriim  7337  resqrexlemgt0  11331  cau3lem  11425  caubnd2  11428  climshftlemg  11613  climcau  11658  climcaucn  11662  serf0  11663  modfsummodlemstep  11768  bezoutlemmain  12319  ctinf  12801  strsetsid  12865  imasaddfnlemg  13146  islss4  14144  fiinbas  14521  baspartn  14522  lmtopcnp  14722  rescncf  15053  limcresi  15138