Theorem cm 61

Description: Commutative inference rule for ortholattices.

Hypothesis

Ref	Expression
cm.1	a = b

Assertion

Ref	Expression
cm	b = a

Proof of Theorem cm

Step	Hyp	Ref	Expression
1		cm.1	. 2 a = b
2	1	ax-r1 35	1 b = a

Syntax hints:   = wb 1

This theorem was proved from axioms:  ax-r1 35

This theorem is referenced by:  k1-6  353  k1-7  354  k1-8a  355  k1-4  359  oa3moa3  1029  mldual  1122  vneulem2  1130  vneulem5  1133  vneulem12  1140  vneulem15  1143  vneulemexp  1146  l42modlem1  1147  dp15lema  1152  dp15lemd  1155  dp15leme  1156  dp15lemg  1158  dp53lema  1161  dp53lemb  1162  dp53lemc  1163  dp53lemd  1164  dp53lemf  1166  dp35leme  1171  dp35lemd  1172  dp35lemc  1173  dp35lemb  1174  dp34  1179  dp41lema  1180  dp41lemb  1181  dp41lemh  1188  dp41lemk  1190  dp41leml  1191  dp32  1194  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35lemc  1209  testmod  1211  testmod2  1213  testmod2expanded  1214  testmod3  1215