Theorem ralimdv 2618

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  poss  4443  sess1  4482  sess2  4483  riinint  5043  dffo4  5856  dffo5  5857  isoini2  6025  rdgivallem  6652  iinerm  6881  xpf1o  7144  exmidontriimlem3  7579  exmidontriim  7581  resqrexlemgt0  11800  cau3lem  11895  caubnd2  11898  climshftlemg  12084  climcau  12129  climcaucn  12133  serf0  12134  modfsummodlemstep  12240  bezoutlemmain  12791  ctinf  13370  strsetsid  13434  imasaddfnlemg  13684  islss4  14768  fiinbas  15199  baspartn  15200  lmtopcnp  15400  rescncf  15731  limcresi  15816  upgrwlkedg  16700  uspgr2wlkeq  16704  umgrwlknloop  16707