Theorem alimdv 1879

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

Syntax hints:   → wi 4  ∀wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1447  ax-gen 1449  ax-17 1526

This theorem is referenced by:  2alimdv  1881  moim  2090  ralimdv2  2547  sstr2  3164  reuss2  3417  ssuni  3833  disjss2  3985  disjss1  3988  disjiun  4000  exmidsssnc  4205  soss  4316  alxfr  4463  ssrel  4716  ssrel2  4718  ssrelrel  4728  iotaval  5191  omnimkv  7156