BetweennessOuterTransitivityFlipped-1
Show Code edit

thm (BetweennessOuterTransitivityFlipped-1 () () (→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (∧ (∧ (between A C x) (≡ C x C D)) (between B C x)))

(∧ (between A C x) (≡ C x C D)) (between A B C) ConjunctionRightElimination

(→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (∧ (between A C x) (≡ C x C D)))

(∧ (between A C x) (≡ C x C D)) (between A B C) ConjunctionLeftElimination

(→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (between A B C))

(∧ (between A C x) (≡ C x C D)) (between A B C) ConjunctionRightElimination

(→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (∧ (between A C x) (≡ C x C D)))

(between A C x) (≡ C x C D) ConjunctionRightElimination

(→ (∧ (between A C x) (≡ C x C D)) (between A C x))

applySyllogism

(→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (between A C x))

composeConjunction

(→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (∧ (between A B C) (between A C x)))

(→ (∧ (between A B C) (between A C x)) (between B C x))

applySyllogism

(→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (between B C x))

composeConjunction

(→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (∧ (∧ (between A C x) (≡ C x C D)) (between B C x)))

)