BetweennessMiddleTransitivityBNotEqualC Show Code edit
thm (BetweennessMiddleTransitivityBNotEqualC () () (→ (¬ (= B C)) (→ (∧ (between A B D) (between B C D)) (between A C D)))
# We'll prove <code>B ≠ C ∧ (between A B D ∧ between B C D) → between A C D</code>, which is only an export away from our desired result.
#
# To apply <code>BetweennessOuterTransitivityFlipped</code> we need three things. The first is <code>between A B C</code>
(¬ (= B C)) (∧ (between A B D) (between B C D)) ConjunctionLeftElimination
(→ (∧ (¬ (= B C)) (∧ (between A B D) (between B C D))) (∧ (between A B D) (between B C D)))
A B D C BetweennessInnerTransitivity
(→ (∧ (between A B D) (between B C D)) (between A B C))
applySyllogism
(→ (∧ (¬ (= B C)) (∧ (between A B D) (between B C D))) (between A B C))
# The second is <code>between B C D</code>
(¬ (= B C)) (∧ (between A B D) (between B C D)) ConjunctionLeftElimination
(→ (∧ (¬ (= B C)) (∧ (between A B D) (between B C D))) (∧ (between A B D) (between B C D)))
eliminateLeftConjunctInConsequent
(→ (∧ (¬ (= B C)) (∧ (between A B D) (between B C D))) (between B C D))
composeConjunction
(→ (∧ (¬ (= B C)) (∧ (between A B D) (between B C D))) (∧ (between A B C) (between B C D)))
# The third is <code>B ≠ C</code>
(¬ (= B C)) (∧ (between A B D) (between B C D)) ConjunctionRightElimination
(→ (∧ (¬ (= B C)) (∧ (between A B D) (between B C D))) (¬ (= B C)))
composeConjunction
(→ (∧ (¬ (= B C)) (∧ (between A B D) (between B C D))) (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))))
A B C D BetweennessOuterTransitivityFlipped
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (between A C D))
applySyllogism
(→ (∧ (¬ (= B C)) (∧ (between A B D) (between B C D))) (between A C D))
export
(→ (¬ (= B C)) (→ (∧ (between A B D) (between B C D)) (between A C D)))
)
edit