Theorem stdpc5v

Description: Version of stdpc5 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020) Revised to shorten 19.21v . (Revised by Wolf Lammen, 12-Jul-2020)

	Ref	Expression
Assertion	stdpc5v	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-5	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		alim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )
3	1 2	syl5	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜓 ) )