Step |
Hyp |
Ref |
Expression |
1 |
|
cgrcomim |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 → 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐴 , 𝐵 〉 ) ) |
2 |
|
cgrcomim |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐴 , 𝐵 〉 → 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) |
3 |
2
|
3com23 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐴 , 𝐵 〉 → 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) |
4 |
1 3
|
impbid |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐶 , 𝐷 〉 ↔ 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐴 , 𝐵 〉 ) ) |