Metamath Proof Explorer

Theorem isoeq145d

Description: Equality deduction for isometries. (Contributed by RP, 14-Jan-2025)

Ref Expression
Hypotheses isoeq145.1 ⊢ φ → F = G
isoeq145.4 ⊢ φ → A = C
isoeq145.5 ⊢ φ → B = D
Assertion isoeq145d ⊢ φ → F Isom R , S A B ↔ G Isom R , S C D

Proof

Step Hyp Ref Expression
1 isoeq145.1 ⊢ φ → F = G
2 isoeq145.4 ⊢ φ → A = C
3 isoeq145.5 ⊢ φ → B = D
4 isoeq1 ⊢ F = G → F Isom R , S A B ↔ G Isom R , S A B
5 1 4 syl ⊢ φ → F Isom R , S A B ↔ G Isom R , S A B
6 isoeq4 ⊢ A = C → G Isom R , S A B ↔ G Isom R , S C B
7 2 6 syl ⊢ φ → G Isom R , S A B ↔ G Isom R , S C B
8 isoeq5 ⊢ B = D → G Isom R , S C B ↔ G Isom R , S C D
9 3 8 syl ⊢ φ → G Isom R , S C B ↔ G Isom R , S C D
10 5 7 9 3bitrd ⊢ φ → F Isom R , S A B ↔ G Isom R , S C D