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. ifptru
14. ifpfal
15. ifpid
16. casesifp
17. ifpbi123d
18. ifpbi23d
19. ifpimpda
20. 1fpid3