![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.43i | Unicode version |
Description: Inference absorbing redundant antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) |
Ref | Expression |
---|---|
pm2.43i.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.43i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm2.43i.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpd 13 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: sylc 62 impbid 129 ibi 176 anidms 397 pm2.13dc 885 hbequid 1513 equidqe 1532 equid 1701 ax10 1717 hbae 1718 vtoclgaf 2802 vtocl2gaf 2804 vtocl3gaf 2806 ifmdc 3574 elinti 3853 copsexg 4244 nlimsucg 4565 tfisi 4586 vtoclr 4674 issref 5011 relresfld 5158 f1o2ndf1 6228 tfrlem9 6319 nndi 6486 mulcanpig 7333 lediv2a 8850 seq3id3 10504 resqrexlemdecn 11016 ndvdssub 11929 nn0seqcvgd 12035 modprm0 12248 fiinopn 13395 xmetunirn 13751 mopnval 13835 ax1hfs 14703 |
Copyright terms: Public domain | W3C validator |