![]() |
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 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.) |
Ref | Expression |
---|---|
trud | ⊢ (𝜑 → ⊤) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1541 | . 2 ⊢ ⊤ | |
2 | 1 | a1i 11 | 1 ⊢ (𝜑 → ⊤) |
Colors of variables: wff setvar class |
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 1905 disjprg 5144 euotd 5523 elabrex 7262 elabrexg 7263 riota5f 7416 bj-abv 36889 wl-2mintru1 37473 wl-nax6im 37499 ac6s6 38159 lhpexle1 39991 prjspvs 42597 cnvtrucl0 43614 rfovcnvf1od 43994 fsupdm 46798 thinciso 48861 |
Copyright terms: Public domain | W3C validator |