Theorem alimdv 1932

Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)

Hypothesis

Ref	Expression
alimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
alimdv	⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem alimdv

Step	Hyp	Ref	Expression
1		ax-17 1579	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	alimdh 1520	1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is referenced by:  2alimdv  1934  moim  2151  ralimdv2  2620  sstr2  3255  reuss2  3513  ssuni  3952  disjss2  4104  disjss1  4107  disjiun  4120  exmidsssnc  4335  soss  4454  alxfr  4602  ssrel  4858  ssrel2  4860  ssrelrel  4870  iotaval  5344  omnimkv  7486