Theorem darapti
"Darapti", one of the syllogisms of Aristotelian logic. All \( \varphi \) is
\( \psi \), all \( \varphi \) is \( \chi \), and some \( \varphi \) exist, therefore some
\( \chi \) is \( \psi \). 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.)
Hypotheses
darapti.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
darapti.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
darapti.e
\( \vdash \exists x \, \varphi \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \psi) \)
Proof
l0
darapti.min
\( \vdash \forall x \, (\varphi \rightarrow \chi) \)
l1
darapti.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
id
alanimi _
\( \vdash \forall x \, (\varphi \rightarrow \chi) \wedge \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, ((\varphi \rightarrow \chi) \wedge (\varphi \rightarrow \psi)) \)
l4
mp2an l0 l1 _
\( \vdash \forall x \, ((\varphi \rightarrow \chi) \wedge (\varphi \rightarrow \psi)) \)
pm3.43
alimi _
\( \vdash \forall x \, ((\varphi \rightarrow \chi) \wedge (\varphi \rightarrow \psi)) \rightarrow \forall x \, (\varphi \rightarrow \chi \wedge \psi) \)
l7
ax-mp l4 _
\( \vdash \forall x \, (\varphi \rightarrow \chi \wedge \psi) \)
l8
darapti.e
\( \vdash \exists x \, \varphi \)
exim
\( \vdash \forall x \, (\varphi \rightarrow \chi \wedge \psi) \rightarrow \exists x \, \varphi \rightarrow \exists x \, (\chi \wedge \psi) \)
mp2 l7 l8 _