Theorem trud 1547

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

Syntax hints:   → wi 4  ⊤wtru 1538

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 1540

This theorem is referenced by:  falimtru  1562  emptyex  1906  disjprg  5162  euotd  5532  elabrex  7279  elabrexg  7280  riota5f  7433  bj-abv  36872  wl-2mintru1  37456  wl-nax6im  37472  ac6s6  38132  lhpexle1  39965  prjspvs  42565  cnvtrucl0  43586  rfovcnvf1od  43966  fsupdm  46763  thinciso  48727