Theorem alsyl

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

Conclusion

\( \vdash \forall x \, (\varphi \rightarrow \psi) \wedge \forall x \, (\psi \rightarrow \chi) \rightarrow \forall x \, (\varphi \rightarrow \chi) \)

Proof

pm3.33

alanimi _