Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > com52l  Unicode version 
Description: Commutation of antecedents. Rotate left twice. (Contributed by Jeff Hankins, 28Jun2009.) 
Ref  Expression 

com5.1 
Ref  Expression 

com52l 
Step  Hyp  Ref  Expression 

1  com5.1  . . 3  
2  1  com5l 88  . 2 
3  2  com5l 88  1 
Colors of variables: wff set class 
Syntax hints: wi 4 
This theorem is referenced by: com52r 91 com5r 92 imp5p 26166 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 8 
Copyright terms: Public domain  W3C validator 