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  1124  mlduali  1126  vneulem3  1131  vneulem6  1134  vneulem7  1135  vneulem9  1137  vneulem11  1139  vneulem12  1140  vneulemexp  1146  dp15lema  1152  dp15lemc  1154  dp15leme  1156  dp15lemf  1157  dp15lemg  1158  dp53lema  1161  dp53lemf  1166  dp35lem0  1177  dp41lemc0  1182  dp41lemf  1186  dp41lemg  1187  dp41lemk  1190  dp32  1194  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod  1211  testmod2  1213  testmod2expanded  1214