Step |
Hyp |
Ref |
Expression |
1 |
|
cvpss |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵 ) ) |
2 |
1
|
3adant3 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵 ) ) |
3 |
|
cvpss |
⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ⋖ℋ 𝐶 → 𝐵 ⊊ 𝐶 ) ) |
4 |
3
|
3adant1 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ⋖ℋ 𝐶 → 𝐵 ⊊ 𝐶 ) ) |
5 |
|
cvnbtwn |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐶 → ¬ ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶 ) ) ) |
6 |
5
|
3com23 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐶 → ¬ ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶 ) ) ) |
7 |
6
|
con2d |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶 ) → ¬ 𝐴 ⋖ℋ 𝐶 ) ) |
8 |
2 4 7
|
syl2and |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ⋖ℋ 𝐵 ∧ 𝐵 ⋖ℋ 𝐶 ) → ¬ 𝐴 ⋖ℋ 𝐶 ) ) |