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 72 | . 2 |
3 | 2 | com12 27 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com13 74 com3l 75 com14 82 expd 245 moexexdc 1984 euexex 1985 mob 2723 issref 4707 relresfld 4847 poxp 5853 nndi 6065 nnmass 6066 distrlem5prl 6684 distrlem5pru 6685 flqeqceilz 9160 ialgcvga 9890 ialgfx 9891 |
Copyright terms: Public domain | W3C validator |