Theorem bamalip
"Bamalip", one of the syllogisms of Aristotelian logic. All \( \varphi \) is
\( \psi \), all \( \psi \) is \( \chi \), and \( \varphi \) exist, therefore some \( \chi \)
is \( \varphi \). In Aristotelian notation, AAI-4: PaM and MaS therefore
SiP. Very similar to barbari. (Contributed by David A. Wheeler,
28-Aug-2016.) Shorten and reduce dependencies on axioms. (Revised by
BJ, 16-Sep-2022.)
Hypotheses
bamalip.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
bamalip.min
\( \vdash \forall x \, (\psi \rightarrow \chi) \)
bamalip.e
\( \vdash \exists x \, \varphi \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \varphi) \)
Proof
l0
bamalip.min
\( \vdash \forall x \, (\psi \rightarrow \chi) \)
l1
bamalip.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
bamalip.e
\( \vdash \exists x \, \varphi \)
l3
barbari l0 l1 _
\( \vdash \exists x \, (\varphi \wedge \chi) \)
exancom
\( \vdash \exists x \, (\varphi \wedge \chi) \leftrightarrow \exists x \, (\chi \wedge \varphi) \)
mpbi l3 _