![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mptru | Unicode version |
Description: Eliminate ![]() ![]() |
Ref | Expression |
---|---|
mptru.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mptru |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1336 |
. 2
![]() ![]() | |
2 | mptru.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-tru 1335 |
This theorem is referenced by: xorbi12i 1362 nfbi 1569 spime 1720 eubii 2009 nfmo 2020 mobii 2037 dvelimc 2303 ralbii 2444 rexbii 2445 nfralxy 2474 nfrexxy 2475 nfralya 2476 nfrexya 2477 nfreuxy 2608 nfsbc1 2930 nfsbc 2933 sbcbii 2972 csbeq2i 3034 nfcsb1 3039 nfcsb 3042 nfif 3505 ssbri 3980 nfbr 3982 mpteq12i 4024 ralxfr 4395 rexxfr 4397 nfiotaw 5100 nfriota 5747 nfov 5809 mpoeq123i 5842 mpoeq3ia 5844 disjsnxp 6142 tfri1 6270 eqer 6469 0er 6471 ecopover 6535 ecopoverg 6538 nfixpxy 6619 en2i 6672 en3i 6673 ener 6681 ensymb 6682 entr 6686 djuf1olem 6946 omp1eomlem 6987 ltsopi 7152 ltsonq 7230 enq0er 7267 ltpopr 7427 ltposr 7595 axcnex 7691 axaddf 7700 axmulf 7701 ltso 7866 nfneg 7983 negiso 8737 sup3exmid 8739 xrltso 9612 frecfzennn 10230 frechashgf1o 10232 0tonninf 10243 1tonninf 10244 facnn 10505 fac0 10506 fac1 10507 cnrecnv 10714 cau3 10919 xrnegiso 11063 sum0 11189 trireciplem 11301 trirecip 11302 ege2le3 11414 oddpwdc 11888 ennnfonelem1 11956 ennnfonelemhf1o 11962 strnfvn 12019 strslss 12045 txswaphmeolem 12528 divcnap 12763 elcncf1ii 12775 cnrehmeocntop 12801 dvid 12870 dveflem 12895 dvef 12896 sincn 12898 coscn 12899 cosz12 12909 sincos6thpi 12971 bj-sbimeh 13150 bdnthALT 13204 012of 13363 2o01f 13364 isomninnlem 13400 iswomninnlem 13417 ismkvnnlem 13419 dceqnconst 13423 iooref1o 13426 taupi 13430 |
Copyright terms: Public domain | W3C validator |