Theorem alimdv 1856

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

Syntax hints:   → wi 4  ∀wal 1330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1424  ax-gen 1426  ax-17 1503

This theorem is referenced by:  2alimdv  1858  moim  2067  ralimdv2  2524  sstr2  3131  reuss2  3383  ssuni  3790  disjss2  3941  disjss1  3944  disjiun  3956  exmidsssnc  4159  soss  4269  alxfr  4415  ssrel  4667  ssrel2  4669  ssrelrel  4679  iotaval  5139  omnimkv  7078