Metamath Proof Explorer


Table of Contents - 21.23.7. Theorems around the conditional operator

  1. wl-ifp-ncond1
  2. wl-ifp-ncond2
  3. wl-ifpimpr
  4. wl-ifp4impr