Theorem dimatis 2712

Description: "Dimatis", one of the syllogisms of Aristotelian logic. Some 𝜑 is 𝜓, and all 𝜓 is 𝜒, therefore some 𝜒 is 𝜑. 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 2689 with positions interchanged. (Contributed by David A. Wheeler, 28-Aug-2016.) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

Hypotheses

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

Assertion

Ref	Expression
dimatis	⊢ ∃𝑥(𝜒 ∧ 𝜑)

Proof of Theorem dimatis

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by: (None)