![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > trud | Unicode version |
Description: Eliminate ![]() ![]() |
Ref | Expression |
---|---|
trud.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
trud |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1246 |
. 2
![]() ![]() | |
2 | trud.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 1245 |
This theorem is referenced by: nfbi 1478 spime 1626 eubii 1906 nfmo 1917 mobii 1934 dvelimc 2195 ralbii 2324 rexbii 2325 nfralxy 2354 nfrexxy 2355 nfralya 2356 nfrexya 2357 nfreuxy 2478 nfsbc1 2775 nfsbc 2778 sbcbii 2812 csbeq2i 2870 nfcsb1 2875 nfcsb 2878 nfif 3350 ssbri 3797 nfbr 3799 mpteq12i 3836 ralxfr 4164 rexxfr 4166 nfiotaxy 4814 nfriota 5420 nfov 5478 mpt2eq123i 5510 mpt2eq3ia 5512 tfri1 5892 eqer 6074 0er 6076 ecopover 6140 ecopoverg 6143 en2i 6186 en3i 6187 ener 6195 ensymb 6196 entr 6200 ltsopi 6304 ltsonq 6382 enq0er 6418 ltpopr 6569 ltposr 6691 axcnex 6745 ltso 6893 nfneg 7005 xrltso 8487 frecfzennn 8884 frechashgf1o 8886 cnrecnv 9138 bj-sbimeh 9247 bdnthALT 9290 |
Copyright terms: Public domain | W3C validator |