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 128 ibi 175 anidms 395 pm2.13dc 871 hbequid 1493 equidqe 1512 equid 1681 ax10 1697 hbae 1698 vtoclgaf 2777 vtocl2gaf 2779 vtocl3gaf 2781 ifmdc 3543 elinti 3818 copsexg 4206 nlimsucg 4527 tfisi 4548 vtoclr 4636 issref 4970 relresfld 5117 f1o2ndf1 6177 tfrlem9 6268 nndi 6435 mulcanpig 7257 lediv2a 8771 seq3id3 10415 resqrexlemdecn 10923 ndvdssub 11833 nn0seqcvgd 11933 modprm0 12144 fiinopn 12472 xmetunirn 12828 mopnval 12912 ax1hfs 13713 |
Copyright terms: Public domain | W3C validator |