![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > trud | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
trud | ⊢ (𝜑 → ⊤) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1538 | . 2 ⊢ ⊤ | |
2 | 1 | a1i 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 |