Metamath Proof Explorer

Theorem caovord2

Description: Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996)

Ref Expression
Hypotheses caovord.1 ⊢ A ∈ V
caovord.2 ⊢ B ∈ V
caovord.3 ⊢ z ∈ S → x R y ↔ z F x R z F y
caovord2.3 ⊢ C ∈ V
caovord2.com ⊢ x F y = y F x
Assertion caovord2 ⊢ C ∈ S → A R B ↔ A F C R B F C

Proof

Step Hyp Ref Expression
1 caovord.1 ⊢ A ∈ V
2 caovord.2 ⊢ B ∈ V
3 caovord.3 ⊢ z ∈ S → x R y ↔ z F x R z F y
4 caovord2.3 ⊢ C ∈ V
5 caovord2.com ⊢ x F y = y F x
6 1 2 3 caovord ⊢ C ∈ S → A R B ↔ C F A R C F B
7 4 1 5 caovcom ⊢ C F A = A F C
8 4 2 5 caovcom ⊢ C F B = B F C
9 7 8 breq12i ⊢ C F A R C F B ↔ A F C R B F C
10 6 9 bitrdi ⊢ C ∈ S → A R B ↔ A F C R B F C