Metamath Proof Explorer


Table of Contents - 20.22.3. Equality deductions

A collection of theorems for commuting equalities (or biimplications) 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