This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
	bamalip.min	⊢ ∀ 𝑥 ( 𝜓 → 𝜒 )
	bamalip.e	⊢ ∃ 𝑥 𝜑
Assertion	bamalip	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bamalip.maj	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
2		bamalip.min	⊢ ∀ 𝑥 ( 𝜓 → 𝜒 )
3		bamalip.e	⊢ ∃ 𝑥 𝜑
4	2 1 3	barbari	⊢ ∃ 𝑥 ( 𝜑 ∧ 𝜒 )
5		exancom	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ↔ ∃ 𝑥 ( 𝜒 ∧ 𝜑 ) )
6	4 5	mpbi	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜑 )