New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > trud | GIF version |
Description: Eliminate ⊤ as an antecedent. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Ref | Expression |
---|---|
trud.1 | ⊢ ( ⊤ → φ) |
Ref | Expression |
---|---|
trud | ⊢ φ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1321 | . 2 ⊢ ⊤ | |
2 | trud.1 | . 2 ⊢ ( ⊤ → φ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ φ |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊤ wtru 1316 |
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 177 df-tru 1319 |
This theorem is referenced by: hadbi123i 1384 cadbi123i 1385 nfn 1793 nfimOLD 1814 nfan 1824 nfbi 1834 nfnfOLD 1846 sbie 2038 eubii 2213 nfeu 2220 nfmo 2221 mobii 2240 dvelimc 2510 ralbii 2638 rexbii 2639 nfral 2667 nfreu 2785 nfrmo 2786 nfrab 2792 nfsbc1 3064 nfsbc 3067 sbcbii 3101 csbeq2i 3162 nfcsb1 3167 nfcsb 3170 nfif 3686 nfiota 4343 nfbr 4683 nfov 5545 mpt2eq123i 5664 mpteq12i 5665 mpt2eq3ia 5670 ider 5943 ssetpov 5944 eqer 5961 ener 6039 lecponc 6213 |
Copyright terms: Public domain | W3C validator |