Theorem trud 1580

Description: Anything implies ⊤. Dual statement of falim 1587. Deduction form of tru 1574. Note on naming: in 2022, the theorem now known as mptru 1577 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1577. (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 1574	. 2 ⊢ ⊤
2	1	a1i 11	1 ⊢ (𝜑 → ⊤)

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1573

This theorem is used by:  falimtru  1595  emptyex  1942  disjprg  5104  euotd  5493  elabrex  7277  elabrexg  7278  riota5f  7436  bj-exextruan  37752  bj-cbvew  37756  bj-abv  38033  wl-2mintru1  38681  wl-nax6im  38718  ac6s6  39370  lhpexle1  41331  prjspvs  43904  cnvtrucl0  44885  rfovcnvf1od  45265  fsupdm  48125  tmachlem-agreeself  48219  thinciso  50936