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  1940  disjprg  5099  euotd  5490  elabrex  7239  elabrexg  7240  riota5f  7398  bj-exextruan  37368  bj-cbvew  37372  bj-abv  37649  wl-2mintru1  38244  wl-nax6im  38281  ac6s6  38920  lhpexle1  40881  prjspvs  43456  cnvtrucl0  44464  rfovcnvf1od  44844  fsupdm  47670  tmachlem-agreeself  47764  thinciso  50396