Theorem ror 71

Description: Inference introducing disjunct to right. (Contributed by NM, 26-May-2008.) (Revised by NM, 31-Mar-2011.)

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 was proved from axioms:  ax-r5 38

This theorem is referenced by:  k1-7  354  k1-8a  355  k1-8b  356  oa3moa3  1029  mli  1126  mlduali  1128  vneulem3  1133  vneulem6  1136  vneulem7  1137  vneulem9  1139  vneulem11  1141  vneulem12  1142  vneulemexp  1148  dp15lema  1154  dp15lemc  1156  dp15leme  1158  dp15lemf  1159  dp15lemg  1160  dp53lema  1163  dp53lemf  1168  dp35lem0  1179  dp41lemc0  1184  dp41lemf  1188  dp41lemg  1189  dp41lemk  1192  dp32  1196  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod  1213  testmod2  1215  testmod2expanded  1216