Description: An alternate definition of "true" (see comment of df-tru ). The associated justification theorem is monothetic . (Contributed by Anthony Hart, 13-Oct-2010) (Revised by BJ, 12-Jul-2019) Use tru instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dftru2 | |- ( T. <-> ( ph -> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tru | |- T. |
|
| 2 | id | |- ( ph -> ph ) |
|
| 3 | 1 2 | 2th | |- ( T. <-> ( ph -> ph ) ) |