Theorem trud 1573

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

Syntax hints:   → wi 4  ⊤wtru 1564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-tru 1566

This theorem is referenced by:  falimtru  1588  emptyex  1930  disjprg  5100  euotd  5486  elabrex  7230  elabrexg  7231  riota5f  7385  bj-exextruan  37117  bj-cbvew  37121  bj-abv  37398  wl-2mintru1  37991  wl-nax6im  38028  ac6s6  38678  lhpexle1  40639  prjspvs  43199  cnvtrucl0  44207  rfovcnvf1od  44587  fsupdm  47415  thinciso  50100