Theorem trud 1548

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

Syntax hints:   → wi 4  ⊤wtru 1539

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 1541

This theorem is referenced by:  falimtru  1563  emptyex  1908  disjprgw  5027  disjprg  5028  euotd  5372  mptexgf  6976  elabrex  6994  riota5f  7136  bj-abv  34627  wl-2mintru1  35187  wl-nax6im  35203  ac6s6  35890  lhpexle1  37584  prjspvs  39946  cnvtrucl0  40697  rfovcnvf1od  41078  elabrexg  42048