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 2083 euexex 2084 mob 2866 issref 4921 relresfld 5068 poxp 6129 nndi 6382 nnmass 6383 pr2ne 7048 distrlem5prl 7394 distrlem5pru 7395 lbreu 8703 flqeqceilz 10091 divconjdvds 11547 algcvga 11732 algfx 11733 fiinopn 12171 |
Copyright terms: Public domain | W3C validator |