Metamath Proof Explorer
Table of Contents - 20.10.37.1. Congruence properties
- cofs
- df-ofs
- cgrrflx2d
- cgrtr4d
- cgrtr4and
- cgrrflx
- cgrrflxd
- cgrcomim
- cgrcom
- cgrcomand
- cgrtr
- cgrtrand
- cgrtr3
- cgrtr3and
- cgrcoml
- cgrcomr
- cgrcomlr
- cgrcomland
- cgrcomrand
- cgrcomlrand
- cgrtriv
- cgrid2
- cgrdegen
- brofs
- 5segofs
- ofscom
- cgrextend
- cgrextendand
- segconeq
- segconeu