Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imim1i | Unicode version |
Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.) |
Ref | Expression |
---|---|
imim1i.1 |
Ref | Expression |
---|---|
imim1i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim1i.1 | . 2 | |
2 | id 19 | . 2 | |
3 | 1, 2 | imim12i 59 | 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: jarr 97 bi3ant 223 pm3.41 329 pm3.42 330 jarl 648 pm2.67-2 703 oibabs 704 stdcn 837 pm2.85dc 895 peircedc 904 3jaob 1291 hbim 1532 hbimd 1560 i19.39 1627 hbae 1705 sbcof2 1797 sb4or 1820 tfi 4556 dmcosseq 4872 fliftfun 5761 tfrcl 6326 ac6sfi 6858 fsum2d 11370 fsumabs 11400 fsumiun 11412 fprod2d 11558 bj-nnsn 13508 bj-pm2.18st 13525 setindis 13742 bdsetindis 13744 |
Copyright terms: Public domain | W3C validator |