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

Theorem trud 1544
Description: Anything implies . Dual statement of falim 1551. Deduction form of tru 1538. Note on naming: in 2022, the theorem now known as mptru 1541 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1541. (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 1538 . 2
21a1i 11 1 (𝜑 → ⊤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1535
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 206  df-tru 1537
This theorem is referenced by:  falimtru  1559  emptyex  1903  disjprgw  5148  disjprg  5149  euotd  5519  elabrex  7257  elabrexg  7258  riota5f  7409  bj-abv  36612  wl-2mintru1  37197  wl-nax6im  37213  ac6s6  37873  lhpexle1  39707  prjspvs  42264  cnvtrucl0  43291  rfovcnvf1od  43671  fsupdm  46463  thinciso  48381
  Copyright terms: Public domain W3C validator