Theorem ralimdv 2558

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

Syntax hints:   → wi 4   ∈ wcel 2160  ∀wral 2468

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  poss  4316  sess1  4355  sess2  4356  riinint  4906  dffo4  5685  dffo5  5686  isoini2  5841  rdgivallem  6406  iinerm  6633  xpf1o  6872  exmidontriimlem3  7252  exmidontriim  7254  resqrexlemgt0  11061  cau3lem  11155  caubnd2  11158  climshftlemg  11342  climcau  11387  climcaucn  11391  serf0  11392  modfsummodlemstep  11497  bezoutlemmain  12031  ctinf  12481  strsetsid  12545  imasaddfnlemg  12791  islss4  13698  fiinbas  14006  baspartn  14007  lmtopcnp  14207  rescncf  14525  limcresi  14592