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

Metamath Proof Explorer

Theorem darii

Description: "Darii", one of the syllogisms of Aristotelian logic. All ph is ps , and some ch is ph , therefore some ch is ps . In Aristotelian notation, AII-1: MaP and SiM therefore SiP. For example, given "All rabbits have fur" and "Some pets are rabbits", therefore "Some pets have fur". Example from https://en.wikipedia.org/wiki/Syllogism . See dariiALT for a shorter proof requiring more axioms. (Contributed by David A. Wheeler, 24-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

Step Hyp Ref Expression
1 darii.maj ⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
2 darii.min ⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜑 )
3 id ⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) )
4 3 anim2d ⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝜒 ∧ 𝜑 ) → ( 𝜒 ∧ 𝜓 ) ) )
5 4 alimi ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( ( 𝜒 ∧ 𝜑 ) → ( 𝜒 ∧ 𝜓 ) ) )
6 1 5 ax-mp ⊢ ∀ 𝑥 ( ( 𝜒 ∧ 𝜑 ) → ( 𝜒 ∧ 𝜓 ) )
7 exim ⊢ ( ∀ 𝑥 ( ( 𝜒 ∧ 𝜑 ) → ( 𝜒 ∧ 𝜓 ) ) → ( ∃ 𝑥 ( 𝜒 ∧ 𝜑 ) → ∃ 𝑥 ( 𝜒 ∧ 𝜓 ) ) )
8 6 2 7 mp2 ⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )