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 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  dplem15a 1148  dplem15d 1151  dplem15e 1152  dplem15g 1154  dp53lema 1157  dp53lemb 1158  dp53lemc 1159  dp53lemd 1160  dp53lemf 1162  dp34 1165  dp41lema 1166  dp41lemb 1167  dp41lemh 1174  dp41lemk 1176  dp41leml 1177  dp32 1180

This theorem was proved from axioms:  ax-r1 35

Copyright terms: Public domain