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

Metamath Proof Explorer

Theorem darapti

Description: "Darapti", one of the syllogisms of Aristotelian logic. All ph is ps , all ph is ch , and some ph exist, therefore some ch is ps . In Aristotelian notation, AAI-3: MaP and MaS therefore SiP. For example, "All squares are rectangles" and "All squares are rhombuses", therefore "Some rhombuses are rectangles". (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

Step Hyp Ref Expression
1 darapti.maj ⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
2 darapti.min ⊢ ∀ 𝑥 ( 𝜑 → 𝜒 )
3 darapti.e ⊢ ∃ 𝑥 𝜑
4 id ⊢ ( ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) → ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) )
5 4 alanimi ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜒 ) ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) → ∀ 𝑥 ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) )
6 2 1 5 mp2an ⊢ ∀ 𝑥 ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) )
7 pm3.43 ⊢ ( ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )
8 7 alimi ⊢ ( ∀ 𝑥 ( ( 𝜑 → 𝜒 ) ∧ ( 𝜑 → 𝜓 ) ) → ∀ 𝑥 ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )
9 6 8 ax-mp ⊢ ∀ 𝑥 ( 𝜑 → ( 𝜒 ∧ 𝜓 ) )
10 exim ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝜒 ∧ 𝜓 ) ) )
11 9 3 10 mp2 ⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )