![]() |
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 2804 vtocl2gaf 2806 vtocl3gaf 2808 ifmdc 3576 elinti 3855 copsexg 4246 nlimsucg 4567 tfisi 4588 vtoclr 4676 issref 5013 relresfld 5160 f1o2ndf1 6231 tfrlem9 6322 nndi 6489 mulcanpig 7336 lediv2a 8854 seq3id3 10509 resqrexlemdecn 11023 ndvdssub 11937 nn0seqcvgd 12043 modprm0 12256 fiinopn 13589 xmetunirn 13943 mopnval 14027 ax1hfs 14907 |
Copyright terms: Public domain | W3C validator |