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: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: sylc 62 impbid 128 ibi 175 anidms 394 pm2.13dc 870 hbequid 1493 equidqe 1512 equid 1677 ax10 1695 hbae 1696 vtoclgaf 2746 vtocl2gaf 2748 vtocl3gaf 2750 ifmdc 3504 elinti 3775 copsexg 4161 nlimsucg 4476 tfisi 4496 vtoclr 4582 issref 4916 relresfld 5063 f1o2ndf1 6118 tfrlem9 6209 nndi 6375 mulcanpig 7136 lediv2a 8646 seq3id3 10273 resqrexlemdecn 10777 ndvdssub 11616 nn0seqcvgd 11711 fiinopn 12160 xmetunirn 12516 mopnval 12600 ax1hfs 13229 |
Copyright terms: Public domain | W3C validator |