Anything implies \( \top \). Dual statement of falim. Deduction form of tru. Note on naming: in 2022, the theorem now known as mptru was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)