Metamath Proof Explorer


Theorem trud

Description: Anything implies T. . 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)

Ref Expression
Assertion trud ( 𝜑 → ⊤ )

Proof

Step Hyp Ref Expression
1 tru
2 1 a1i ( 𝜑 → ⊤ )