Theorem trud 1532

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

Assertion

Ref	Expression
trud	⊢ (𝜑 → ⊤)

Proof of Theorem trud

Step	Hyp	Ref	Expression
1		tru 1526	. 2 ⊢ ⊤
2	1	a1i 11	1 ⊢ (𝜑 → ⊤)

Syntax hints:   → wi 4  ⊤wtru 1523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-tru 1525

This theorem is referenced by:  falimtru  1547  disjprg  4958  euotd  5294  mptexgf  6851  elabrex  6867  riota5f  7002  wl-nax6im  34308  wl-nax6al  34309  ac6s6  35001  lhpexle1  36694  prjspvs  38776  cnvtrucl0  39488  rfovcnvf1od  39854  elabrexg  40861