Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > com3r | Unicode version |
Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.) |
Ref | Expression |
---|---|
com3.1 |
Ref | Expression |
---|---|
com3r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com3.1 | . . 3 | |
2 | 1 | com23 78 | . 2 |
3 | 2 | com12 30 | 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: com13 80 com3l 81 com14 88 expd 256 moexexdc 2081 euexex 2082 mob 2861 issref 4916 relresfld 5063 poxp 6122 nndi 6375 nnmass 6376 pr2ne 7041 distrlem5prl 7387 distrlem5pru 7388 lbreu 8696 flqeqceilz 10084 divconjdvds 11536 algcvga 11721 algfx 11722 fiinopn 12160 |
Copyright terms: Public domain | W3C validator |