Theorem barbara

"Barbara", one of the fundamental syllogisms of Aristotelian logic. All \( \varphi \) is \( \psi \), and all \( \chi \) is \( \varphi \), therefore all \( \chi \) is \( \psi \). In Aristotelian notation, AAA-1: MaP and SaM therefore SaP. For example, given "All men are mortal" and "Socrates is a man", we can prove "Socrates is mortal". If H is the set of men, M is the set of mortal beings, and S is Socrates, these word phrases can be represented as A. x ( x e. H -> x e. M ) (all men are mortal) and A. x ( x = S -> x e. H ) (Socrates is a man) therefore A. x ( x = S -> x e. M ) (Socrates is mortal). Russell and Whitehead note that "the syllogism in Barbara [ barbara ] is derived from [ syl ]" (quote after Theorem *2.06 of [WhiteheadRussell] p. 101). Most of the proof is in alsyl. There are a legion of sources for Barbara, including http://www.friesian.com/aristotl.htm, http://plato.stanford.edu/entries/aristotle-logic/, and https://en.wikipedia.org/wiki/Syllogism. (Contributed by David A. Wheeler, 24-Aug-2016.)

Hypotheses
barbara.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
barbara.min
\( \vdash \forall x \, (\chi \rightarrow \varphi) \)
Conclusion
\( \vdash \forall x \, (\chi \rightarrow \psi) \)
Proof
l0
barbara.min
\( \vdash \forall x \, (\chi \rightarrow \varphi) \)
l1
barbara.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
alsyl
\( \vdash \forall x \, (\chi \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, (\chi \rightarrow \psi) \)
mp2an l0 l1 _