Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > com4t | Structured version Visualization version Unicode version |
Description: Commutation of antecedents. Rotate twice. (Contributed by NM, 25-Apr-1994.) |
Ref | Expression |
---|---|
com4.1 |
Ref | Expression |
---|---|
com4t |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com4.1 | . . 3 | |
2 | 1 | com4l 92 | . 2 |
3 | 2 | com4l 92 | 1 |
Colors of variables: wff setvar 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: com4r 94 com24 95 isofrlem 6590 tfindsg 7060 tfr3 7495 pssnn 8178 dfac5 8951 cfcoflem 9094 isf32lem12 9186 ltexprlem7 9864 dirtr 17236 erclwwlkstr 26936 erclwwlksntr 26948 3cyclfrgrrn1 27149 frgrregord013 27253 chirredlem1 29249 mdsymlem4 29265 cdj3lem2b 29296 ssfz12 41324 |
Copyright terms: Public domain | W3C validator |