Theorem trud 1579

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

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

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 1572

This theorem is used by:  falimtru  1594  emptyex  1939  disjprg  5098  euotd  5485  elabrex  7247  elabrexg  7248  riota5f  7406  bj-exextruan  37630  bj-cbvew  37634  bj-abv  37911  wl-2mintru1  38507  wl-nax6im  38544  ac6s6  39198  lhpexle1  41159  prjspvs  43732  cnvtrucl0  44718  rfovcnvf1od  45098  fsupdm  47946  tmachlem-agreeself  48040  thinciso  50699