Theorem cm 61

Description: Commutative inference rule for ortholattices. (Contributed by NM, 26-May-2008.)

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  1124  vneulem2  1132  vneulem5  1135  vneulem12  1142  vneulem15  1145  vneulemexp  1148  l42modlem1  1149  dp15lema  1154  dp15lemd  1157  dp15leme  1158  dp15lemg  1160  dp53lema  1163  dp53lemb  1164  dp53lemc  1165  dp53lemd  1166  dp53lemf  1168  dp35leme  1173  dp35lemd  1174  dp35lemc  1175  dp35lemb  1176  dp34  1181  dp41lema  1182  dp41lemb  1183  dp41lemh  1190  dp41lemk  1192  dp41leml  1193  dp32  1196  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211  testmod  1213  testmod2  1215  testmod2expanded  1216  testmod3  1217