Theorem dimatis 2570

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 2553 with positions interchanged. (Contributed by David A. Wheeler, 28-Aug-2016.)

Hypotheses

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

Assertion

Ref	Expression
dimatis	⊢ ∃𝑥(𝜒 ∧ 𝜑)

Proof of Theorem dimatis

Step	Hyp	Ref	Expression
1		dimatis.maj	. 2 ⊢ ∃𝑥(𝜑 ∧ 𝜓)
2		dimatis.min	. . . . 5 ⊢ ∀𝑥(𝜓 → 𝜒)
3	2	spi 2042	. . . 4 ⊢ (𝜓 → 𝜒)
4	3	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
5		simpl 472	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
6	4, 5	jca 553	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜑))
7	1, 6	eximii 1754	1 ⊢ ∃𝑥(𝜒 ∧ 𝜑)

Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by: (None)