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

Theorem trud 1550
Description: Anything implies . Dual statement of falim 1557. Deduction form of tru 1544. Note on naming: in 2022, the theorem now known as mptru 1547 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1547. (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 1544 . 2
21a1i 11 1 (𝜑 → ⊤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1541
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 1543
This theorem is referenced by:  falimtru  1565  emptyex  1907  disjprg  5139  euotd  5518  elabrex  7262  elabrexg  7263  riota5f  7416  bj-abv  36907  wl-2mintru1  37491  wl-nax6im  37519  ac6s6  38179  lhpexle1  40010  prjspvs  42620  cnvtrucl0  43637  rfovcnvf1od  44017  fsupdm  46857  thinciso  49117
  Copyright terms: Public domain W3C validator