Theorem ralimdv 2612

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

Syntax hints:   → wi 4   ∈ wcel 2205  ∀wral 2522

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 2527

This theorem is referenced by:  poss  4425  sess1  4464  sess2  4465  riinint  5024  dffo4  5831  dffo5  5832  isoini2  5999  rdgivallem  6626  iinerm  6855  xpf1o  7111  exmidontriimlem3  7544  exmidontriim  7546  resqrexlemgt0  11735  cau3lem  11829  caubnd2  11832  climshftlemg  12017  climcau  12062  climcaucn  12066  serf0  12067  modfsummodlemstep  12173  bezoutlemmain  12724  ctinf  13270  strsetsid  13334  imasaddfnlemg  13583  islss4  14661  fiinbas  15045  baspartn  15046  lmtopcnp  15246  rescncf  15577  limcresi  15662  upgrwlkedg  16487  uspgr2wlkeq  16491  umgrwlknloop  16494