Metamath Proof Explorer

Table of Contents - 21.24.3. Equality deductions

A collection of theorems for commuting equalities (or biconditionals) with other constructs.

1. iuneq2f
2. rabeq12f
3. csbeq12
4. sbeqi
5. ralbi12f
6. oprabbi
7. mpobi123f
8. iuneq12f
9. iineq12f
10. opabbi
11. mptbi12f