Theorem dimatis

Description: "Dimatis", one of the syllogisms of Aristotelian logic. Some ph is ps , and all ps is ch , therefore some ch is ph . In Aristotelian notation, IAI-4: PiM and MaS therefore SiP. For example, "Some pets are rabbits", "All rabbits have fur", therefore "Some fur bearing animals are pets". Like darii with positions interchanged. (Contributed by David A. Wheeler, 28-Aug-2016) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

	Ref	Expression
Hypotheses	dimatis.maj	⊢ ∃ 𝑥 ( 𝜑 ∧ 𝜓 )
	dimatis.min	⊢ ∀ 𝑥 ( 𝜓 → 𝜒 )
Assertion	dimatis	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜑 )

Proof

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