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))))

(→ (∧ (∧ (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)))

)