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  7240  elabrexg  7241  riota5f  7399  bj-exextruan  37371  bj-cbvew  37375  bj-abv  37652  wl-2mintru1  38247  wl-nax6im  38284  ac6s6  38923  lhpexle1  40884  prjspvs  43459  cnvtrucl0  44467  rfovcnvf1od  44847  fsupdm  47673  tmachlem-agreeself  47767  thinciso  50399