![]() |
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 2803 vtocl2gaf 2805 vtocl3gaf 2807 ifmdc 3575 elinti 3854 copsexg 4245 nlimsucg 4566 tfisi 4587 vtoclr 4675 issref 5012 relresfld 5159 f1o2ndf1 6229 tfrlem9 6320 nndi 6487 mulcanpig 7334 lediv2a 8852 seq3id3 10507 resqrexlemdecn 11021 ndvdssub 11935 nn0seqcvgd 12041 modprm0 12254 fiinopn 13507 xmetunirn 13861 mopnval 13945 ax1hfs 14824 |
Copyright terms: Public domain | W3C validator |