Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > trud | GIF version |
Description: Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Ref | Expression |
---|---|
trud.1 | ⊢ (⊤ → 𝜑) |
Ref | Expression |
---|---|
trud | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1247 | . 2 ⊢ ⊤ | |
2 | trud.1 | . 2 ⊢ (⊤ → 𝜑) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊤wtru 1244 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-tru 1246 |
This theorem is referenced by: xorbi12i 1274 nfbi 1481 spime 1629 eubii 1909 nfmo 1920 mobii 1937 dvelimc 2198 ralbii 2330 rexbii 2331 nfralxy 2360 nfrexxy 2361 nfralya 2362 nfrexya 2363 nfreuxy 2484 nfsbc1 2781 nfsbc 2784 sbcbii 2818 csbeq2i 2876 nfcsb1 2881 nfcsb 2884 nfif 3356 ssbri 3806 nfbr 3808 mpteq12i 3845 ralxfr 4198 rexxfr 4200 nfiotaxy 4871 nfriota 5477 nfov 5535 mpt2eq123i 5568 mpt2eq3ia 5570 tfri1 5951 eqer 6138 0er 6140 ecopover 6204 ecopoverg 6207 en2i 6250 en3i 6251 ener 6259 ensymb 6260 entr 6264 ltsopi 6418 ltsonq 6496 enq0er 6533 ltpopr 6693 ltposr 6848 axcnex 6935 ltso 7096 nfneg 7208 xrltso 8717 frecfzennn 9203 frechashgf1o 9205 cnrecnv 9510 cau3 9711 bj-sbimeh 9912 bdnthALT 9955 |
Copyright terms: Public domain | W3C validator |