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 𝑥 ( 𝜒𝜓 )