Theorem ralimdv 2576

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

Syntax hints:   → wi 4   ∈ wcel 2178  ∀wral 2486

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  poss  4363  sess1  4402  sess2  4403  riinint  4958  dffo4  5751  dffo5  5752  isoini2  5911  rdgivallem  6490  iinerm  6717  xpf1o  6966  exmidontriimlem3  7366  exmidontriim  7368  resqrexlemgt0  11446  cau3lem  11540  caubnd2  11543  climshftlemg  11728  climcau  11773  climcaucn  11777  serf0  11778  modfsummodlemstep  11883  bezoutlemmain  12434  ctinf  12916  strsetsid  12980  imasaddfnlemg  13261  islss4  14259  fiinbas  14636  baspartn  14637  lmtopcnp  14837  rescncf  15168  limcresi  15253