Theorem ralimdv 2565

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  poss  4333  sess1  4372  sess2  4373  riinint  4927  dffo4  5710  dffo5  5711  isoini2  5866  rdgivallem  6439  iinerm  6666  xpf1o  6905  exmidontriimlem3  7290  exmidontriim  7292  resqrexlemgt0  11185  cau3lem  11279  caubnd2  11282  climshftlemg  11467  climcau  11512  climcaucn  11516  serf0  11517  modfsummodlemstep  11622  bezoutlemmain  12165  ctinf  12647  strsetsid  12711  imasaddfnlemg  12957  islss4  13938  fiinbas  14285  baspartn  14286  lmtopcnp  14486  rescncf  14817  limcresi  14902