Theorem ralimdv 2610

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

Syntax hints:   → wi 4   ∈ wcel 2203  ∀wral 2520

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 2525

This theorem is referenced by:  poss  4419  sess1  4458  sess2  4459  riinint  5018  dffo4  5825  dffo5  5826  isoini2  5992  rdgivallem  6612  iinerm  6841  xpf1o  7097  exmidontriimlem3  7530  exmidontriim  7532  resqrexlemgt0  11705  cau3lem  11799  caubnd2  11802  climshftlemg  11987  climcau  12032  climcaucn  12036  serf0  12037  modfsummodlemstep  12143  bezoutlemmain  12694  ctinf  13181  strsetsid  13245  imasaddfnlemg  13527  islss4  14530  fiinbas  14914  baspartn  14915  lmtopcnp  15115  rescncf  15446  limcresi  15531  upgrwlkedg  16356  uspgr2wlkeq  16360  umgrwlknloop  16363