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. ifpdfbiOLD
11. anifp
12. ifpor
13. ifpn
14. ifptru
15. ifpfal
16. ifpid
17. casesifp
18. ifpbi123d
19. ifpbi23d
20. ifpimpda
21. 1fpid3