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)))
A B C x BetweennessInnerTransitivityFlipped
(→ (∧ (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)))
)
edit