Theorem lor 70

Description: Inference introducing disjunct to left. (Contributed by NM, 10-Aug-1997.)

Hypothesis

Ref	Expression
lor.1	a = b

Assertion

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

Proof of Theorem lor

Step	Hyp	Ref	Expression
1		lor.1	. . 3 a = b
2	1	ax-r5 38	. 2 (a ∪ c) = (b ∪ c)
3		ax-a2 31	. 2 (c ∪ a) = (a ∪ c)
4		ax-a2 31	. 2 (c ∪ b) = (b ∪ c)
5	2, 3, 4	3tr1 63	1 (c ∪ a) = (c ∪ b)

Syntax hints:   = wb 1   ∪ wo 6

This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36  ax-r5 38

This theorem is referenced by:  2or  72  anass  76  lan  77  or32  82  or4  84  or42  85  anor1  88  or0  102  or1  104  an1  106  an0  108  oridm  110  orordir  113  orabs  120  conb  122  leao  124  di  126  wwoml2  212  wwoml3  213  anorabs  225  ka4lemo  228  sklem  230  ska3  232  lei3  246  mccune2  247  ni31  250  li3  252  ud1lem0a  255  ud2lem0b  259  ud4lem0a  262  i1i2  266  0i1  273  i1id  275  i2id  276  ud1lem0c  277  wql2lem2  289  wql2lem3  290  wql2lem5  292  wql1  293  oaidlem1  294  womle2a  295  nomb41  299  nomb32  300  nomcon1  302  nomcon2  303  nom11  308  nom12  309  nom13  310  nom14  311  nom21  314  nom22  315  nom23  316  nom50  331  nom51  332  nom52  333  nom53  334  nom54  335  k1-7  354  k1-5  360  2vwomr2  362  2vwomlem  365  wr5-2v  366  ska2  432  ska4  433  ka4ot  435  woml6  436  lem3a.1  444  omln  446  omla  447  oml5  449  oml5a  450  oml2  451  oml3  452  comcom  453  com3i  467  fh3  471  fh4  472  fh4c  478  gsth  489  gsth2  490  i0cmtrcom  495  i3bi  496  df2i3  498  dfi4b  500  i3n2  501  oi3ai3  503  i3lem3  506  lem4  511  i3abs1  522  i3th1  543  i3con  551  ud1lem1  560  ud1lem3  562  ud2lem1  563  ud2lem2  564  ud2lem3  565  ud3lem1c  568  ud3lem1  570  ud3lem2  571  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1c  579  ud4lem1  581  ud4lem2  582  ud4lem3b  584  ud4lem3  585  ud5lem1a  586  ud5lem1  589  ud5lem3a  591  ud5lem3  594  u1lemanb  615  u1lemoa  620  u2lemoa  621  u3lemoa  622  u4lemoa  623  u5lemoa  624  u4lemona  628  u5lemona  629  u2lemob  631  u3lemob  632  u4lemob  633  u1lemonb  635  u2lemonb  636  u3lemonb  637  u4lemonb  638  u5lemonb  639  u1lemnaa  640  u3lemnana  647  u5lemnana  649  u3lemc4  703  u4lemc4  704  u1lembi  720  u2lembi  721  i2bi  722  u1lem3var1  731  oi3oa3  733  u2lem1  735  u4lem1  737  u2lem2  745  u1lem3  749  u3lem3n  754  u4lem3n  755  u5lem3n  756  u1lem4  757  u4lem4  759  u5lem4  760  u1lem5  761  u2lem5  762  u4lem5  764  u3lem6  767  u4lem6  768  u24lem  770  u12lem  771  u1lem7  772  u2lem7  773  u3lem7  774  u1lem11  780  u3lem8  783  u3lem9  784  u3lem10  785  u3lem11  786  u3lem11a  787  u3lem13a  789  u3lem13b  790  u3lemax4  796  u3lemax5  797  bi1o1a  798  i2i1i1  800  i1abs  801  test  802  test2  803  3vth1  804  3vth4  807  3vth5  808  3vth6  809  3vth7  810  3vth9  812  3vded11  814  3vded21  817  3vded3  819  1oaii  824  2oalem1  825  2oath1  826  3vroa  831  orbi  842  mlaconj4  844  i1orni1  847  negant2  858  negantlem10  861  neg3antlem2  865  elimconslem  867  elimcons  868  elimcons2  869  comanblem1  870  comanb  872  mhlemlem2  875  mhlem  876  mhlem1  877  mh  879  mlaconjolem  885  mlaconjo  886  cancellem  891  e2ast2  894  e2astlem1  895  govar  896  gomaex3lem1  914  oaidlem2  931  oaidlem2g  932  oa6v4v  933  oa4v3v  934  oa3to4lem1  945  oa3to4lem2  946  oa3to4lem5  949  oa3to4lem6  950  oa6to4  958  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa8to5  972  oa4to4u  973  oa4uto4g  975  oa3-2lema  978  oa3-2lemb  979  oa3-6lem  980  oa3-3lem  981  oa3-1lem  982  oa3-4lem  983  oa3-5lem  984  oa3-u1lem  985  oa3-u2lem  986  oa3-2to2s  990  oalii  1002  oaliv  1003  oalem2  1006  oagen1  1014  oadistc  1022  oa3moa3  1029  4oagen1  1042  lem3.3.3lem2  1050  lem3.3.3  1052  lem3.3.4  1053  lem3.3.6  1056  lem3.3.7i0e1  1057  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem4.6.2e1  1082  lem4.6.6i1j3  1094  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  wdcom  1105  wdwom  1106  mldual  1124  ml2i  1125  mldual2i  1127  ml3le  1129  vneulem5  1135  vneulem12  1142  vneulem13  1143  vneulemexp  1148  l42modlem1  1149  dp15lema  1154  dp15lemc  1156  dp15lemd  1157  dp53lema  1163  dp53lemb  1164  dp53lemc  1165  dp35leme  1173  dp35lemc  1175  dp35lemb  1176  dp41lemd  1186  dp41leme  1187  dp41lemf  1188  dp41lemg  1189  dp41lemj  1191  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211  testmod1  1214  testmod2  1215  testmod2expanded  1216