Metamath Proof Explorer


Table of Contents - 1.2.9. The conditional operator for propositions

This subsection introduces the conditional operator for propositions, denoted by (see df-ifp). It is the analogue for propositions of the conditional operator for classes, denoted by (see df-if).

  1. wif
  2. df-ifp
  3. dfifp2
  4. dfifp3
  5. dfifp4
  6. dfifp5
  7. dfifp6
  8. dfifp7
  9. ifpdfbi
  10. anifp
  11. ifpor
  12. ifpn
  13. ifpnOLD
  14. ifptru
  15. ifpfal
  16. ifpid
  17. casesifp
  18. ifpbi123d
  19. ifpbi123dOLD
  20. ifpbi23d
  21. ifpimpda
  22. 1fpid3