Metamath Proof Explorer

Table of Contents - 21.20.1.8. The conditional operator for propositions

  1. bj-consensus
  2. bj-consensusALT
  3. bj-df-ifc
  4. bj-dfif
  5. bj-ififc