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  5486  elabrex  7244  elabrexg  7245  riota5f  7403  bj-exextruan  37517  bj-cbvew  37521  bj-abv  37798  wl-2mintru1  38393  wl-nax6im  38430  ac6s6  39084  lhpexle1  41045  prjspvs  43618  cnvtrucl0  44609  rfovcnvf1od  44989  fsupdm  47821  tmachlem-agreeself  47915  thinciso  50547