Theorem alsyl

Description: Universally quantified and uncurried (imported) form of syllogism. Theorem *10.3 in WhiteheadRussell p. 150. (Contributed by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Assertion	alsyl	$$⊢\left(\forall x\left(\phi \to \psi \right)\wedge \forall x\left(\psi \to \chi \right)\right)\to \forall x\left(\phi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		pm3.33	$$⊢\left(\left(\phi \to \psi \right)\wedge \left(\psi \to \chi \right)\right)\to \left(\phi \to \chi \right)$$
2	1	alanimi	$$⊢\left(\forall x\left(\phi \to \psi \right)\wedge \forall x\left(\psi \to \chi \right)\right)\to \forall x\left(\phi \to \chi \right)$$