Metamath Proof Explorer


Theorem bamalip

Description: "Bamalip", one of the syllogisms of Aristotelian logic. All ph is ps , all ps is ch , and ph exist, therefore some ch is ph . 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)

Ref Expression
Hypotheses bamalip.maj x φ ψ
bamalip.min x ψ χ
bamalip.e x φ
Assertion bamalip x χ φ

Proof

Step Hyp Ref Expression
1 bamalip.maj x φ ψ
2 bamalip.min x ψ χ
3 bamalip.e x φ
4 2 1 3 barbari x φ χ
5 exancom x φ χ x χ φ
6 4 5 mpbi x χ φ