Theorem alimdv 1927

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 1575	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	alimdh 1516	1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498  ax-17 1575

This theorem is referenced by:  2alimdv  1929  moim  2144  ralimdv2  2603  sstr2  3235  reuss2  3489  ssuni  3920  disjss2  4072  disjss1  4075  disjiun  4088  exmidsssnc  4299  soss  4417  alxfr  4564  ssrel  4820  ssrel2  4822  ssrelrel  4832  iotaval  5305  omnimkv  7415