Theorem ralimdv 2600

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  poss  4395  sess1  4434  sess2  4435  riinint  4993  dffo4  5795  dffo5  5796  isoini2  5960  rdgivallem  6547  iinerm  6776  xpf1o  7030  exmidontriimlem3  7438  exmidontriim  7440  resqrexlemgt0  11585  cau3lem  11679  caubnd2  11682  climshftlemg  11867  climcau  11912  climcaucn  11916  serf0  11917  modfsummodlemstep  12023  bezoutlemmain  12574  ctinf  13056  strsetsid  13120  imasaddfnlemg  13402  islss4  14402  fiinbas  14779  baspartn  14780  lmtopcnp  14980  rescncf  15311  limcresi  15396  upgrwlkedg  16218  uspgr2wlkeq  16222  umgrwlknloop  16225