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  4334  sess1  4373  sess2  4374  riinint  4928  dffo4  5713  dffo5  5714  isoini2  5869  rdgivallem  6448  iinerm  6675  xpf1o  6914  exmidontriimlem3  7308  exmidontriim  7310  resqrexlemgt0  11204  cau3lem  11298  caubnd2  11301  climshftlemg  11486  climcau  11531  climcaucn  11535  serf0  11536  modfsummodlemstep  11641  bezoutlemmain  12192  ctinf  12674  strsetsid  12738  imasaddfnlemg  13018  islss4  14016  fiinbas  14393  baspartn  14394  lmtopcnp  14594  rescncf  14925  limcresi  15010