Theorem ror 71

Description: Inference introducing disjunct to right.

Hypothesis

Ref	Expression
lor.1	a = b

Assertion

Ref	Expression
ror	(a ∪ c) = (b ∪ c)

Proof of Theorem ror

Step	Hyp	Ref	Expression
1		lor.1	. 2 a = b
2	1	ax-r5 38	1 (a ∪ c) = (b ∪ c)

Syntax hints:   = wb 1   ∪ wo 6

This theorem is referenced by:  k1-7 354  k1-8a 355  k1-8b 356

This theorem was proved from axioms:  ax-r5 38

Copyright terms: Public domain