MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trud Structured version   Visualization version   GIF version

Theorem trud 1551
Description: Anything implies . Dual statement of falim 1558. Deduction form of tru 1545. Note on naming: in 2022, the theorem now known as mptru 1548 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1548. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
Assertion
Ref Expression
trud (𝜑 → ⊤)

Proof of Theorem trud
StepHypRef Expression
1 tru 1545 . 2
21a1i 11 1 (𝜑 → ⊤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1542
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 1544
This theorem is referenced by:  falimtru  1566  emptyex  1908  disjprg  5085  euotd  5451  elabrex  7171  elabrexg  7172  riota5f  7326  bj-abv  36919  wl-2mintru1  37503  wl-nax6im  37531  ac6s6  38191  lhpexle1  40026  prjspvs  42622  cnvtrucl0  43636  rfovcnvf1od  44016  fsupdm  46859  thinciso  49481
  Copyright terms: Public domain W3C validator