Theorem ralimdv 2598

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  poss  4393  sess1  4432  sess2  4433  riinint  4991  dffo4  5791  dffo5  5792  isoini2  5955  rdgivallem  6542  iinerm  6771  xpf1o  7025  exmidontriimlem3  7428  exmidontriim  7430  resqrexlemgt0  11571  cau3lem  11665  caubnd2  11668  climshftlemg  11853  climcau  11898  climcaucn  11902  serf0  11903  modfsummodlemstep  12008  bezoutlemmain  12559  ctinf  13041  strsetsid  13105  imasaddfnlemg  13387  islss4  14386  fiinbas  14763  baspartn  14764  lmtopcnp  14964  rescncf  15295  limcresi  15380  upgrwlkedg  16158  uspgr2wlkeq  16162  umgrwlknloop  16165