![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.43i | GIF 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 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 8851 seq3id3 10506 resqrexlemdecn 11020 ndvdssub 11934 nn0seqcvgd 12040 modprm0 12253 fiinopn 13474 xmetunirn 13828 mopnval 13912 ax1hfs 14791 |
Copyright terms: Public domain | W3C validator |