This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sylg

Description: A syllogism combined with generalization. Inference associated with sylgt . General form of alrimih . (Contributed by NM, 9-Jan-1993) Extract from proof of alrimih . (Revised by BJ, 4-Oct-2019)

	Ref	Expression
Hypotheses	sylg.1	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
	sylg.2	⊢ ( 𝜓 → 𝜒 )
Assertion	sylg	⊢ ( 𝜑 → ∀ 𝑥 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		sylg.1	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
2		sylg.2	⊢ ( 𝜓 → 𝜒 )
3	2	alimi	⊢ ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 )
4	1 3	syl	⊢ ( 𝜑 → ∀ 𝑥 𝜒 )