Theorem dimatis 2320

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

Hypotheses

Ref	Expression
dimatis.maj	⊢ ∃x(φ ∧ ψ)
dimatis.min	⊢ ∀x(ψ → χ)

Assertion

Ref	Expression
dimatis	⊢ ∃x(χ ∧ φ)

Proof of Theorem dimatis

Step	Hyp	Ref	Expression
1		dimatis.maj	. 2 ⊢ ∃x(φ ∧ ψ)
2		dimatis.min	. . . . . 6 ⊢ ∀x(ψ → χ)
3	2	spi 1753	. . . . 5 ⊢ (ψ → χ)
4	3	adantl 452	. . . 4 ⊢ ((φ ∧ ψ) → χ)
5		simpl 443	. . . 4 ⊢ ((φ ∧ ψ) → φ)
6	4, 5	jca 518	. . 3 ⊢ ((φ ∧ ψ) → (χ ∧ φ))
7	6	eximi 1576	. 2 ⊢ (∃x(φ ∧ ψ) → ∃x(χ ∧ φ))
8	1, 7	ax-mp 5	1 ⊢ ∃x(χ ∧ φ)

Syntax hints:   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542

This theorem is referenced by: (None)