Theorem trud 1552

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

Syntax hints:   → wi 4  ⊤wtru 1543

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 207  df-tru 1545

This theorem is referenced by:  falimtru  1567  emptyex  1909  disjprg  5082  euotd  5461  elabrex  7190  elabrexg  7191  riota5f  7345  bj-exextruan  36948  bj-cbvew  36952  bj-abv  37229  wl-2mintru1  37820  wl-nax6im  37857  ac6s6  38507  lhpexle1  40468  prjspvs  43057  cnvtrucl0  44069  rfovcnvf1od  44449  fsupdm  47288  thinciso  49957