Theorem 2or 72

Description: Join both sides with disjunction. (Contributed by NM, 10-Aug-1997.)

Hypotheses

Ref	Expression
2or.1	a = b
2or.2	c = d

Assertion

Ref	Expression
2or	(a ∪ c) = (b ∪ d)

Proof of Theorem 2or

Step	Hyp	Ref	Expression
1		2or.2	. . 3 c = d
2	1	lor 70	. 2 (a ∪ c) = (a ∪ d)
3		2or.1	. . 3 a = b
4	3	ax-r5 38	. 2 (a ∪ d) = (b ∪ d)
5	2, 4	ax-r2 36	1 (a ∪ c) = (b ∪ d)

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:  oran  87  dfb  94  bicom  96  lbi  97  biid  116  1b  117  mi  125  omlem1  127  omlem2  128  ledir  175  comm0  178  comm1  179  bctr  181  cbtr  182  cmtrcom  190  wlem3.1  210  wwfh1  216  wwfh3  218  wwfh4  219  ka4lem  229  lei3  246  mccune2  247  i3n1  249  i3id  251  li3  252  ri3  253  ud1lem0b  256  ud2lem0a  258  ud4lem0a  262  ud4lem0b  263  ud5lem0a  264  ud5lem0b  265  i3i4  270  i5con  272  1i1  274  womle2a  295  nomcon2  303  nom15  312  nom24  317  nom25  318  nom40  325  nom51  332  nom53  334  k1-2  357  k1-3  358  k1-4  359  k1-5  360  2vwomr2  362  wdf-c2  384  wcom2or  427  ska2  432  ska4  433  wom2  434  ka4ot  435  woml6  436  woml7  437  comcom  453  comcom5  458  comdr  466  df2c1  468  fh1  469  fh1r  473  fh2r  474  com2or  483  oml4  487  gsth  489  comcmtr1  494  i3bi  496  dfi3b  499  dfi4b  500  i3n2  501  i3lem1  504  i3lem3  506  lem4  511  i3abs1  522  i3abs3  524  i3con  551  ud1lem1  560  ud1lem3  562  ud2lem1  563  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1d  569  ud3lem1  570  ud3lem2  571  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud4lem2  582  ud4lem3  585  ud5lem1a  586  ud5lem1b  587  ud5lem1  589  ud5lem2  590  ud5lem3a  591  ud5lem3b  592  ud5lem3  594  u1lemaa  600  u2lemaa  601  u3lemaa  602  u4lemaa  603  u5lemaa  604  u2lemana  606  u3lemana  607  u4lemana  608  u5lemana  609  u3lemab  612  u4lemab  613  u5lemab  614  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u3lemob  632  u3lemonb  637  u3lemnana  647  u5lemnana  649  u4lemnab  653  u5lemnab  654  u2lemnoa  661  u3lemnoa  662  u4lemnoa  663  u5lemnoa  664  u1lemnonb  675  u3lemnonb  677  u4lemnonb  678  u5lemnonb  679  u3lemc4  703  u4lemc4  704  i1com  708  u1lemle2  715  u4lemle2  718  u5lemle2  719  u5lembi  725  u12lembi  726  u21lembi  727  u1lemn1b  730  oi3oa3lem1  732  u4lem1  737  u3lem1n  741  u4lem1n  742  u5lem1n  743  u1lem2  744  u1lem3  749  u3lem3  751  u4lem3  752  u5lem3  753  u3lem3n  754  u4lem3n  755  u5lem3n  756  u4lem4  759  u4lem5  764  u4lem6  768  u24lem  770  u12lem  771  u2lem7  773  u3lem7  774  u2lem7n  775  u1lem8  776  u1lem11  780  u2lem8  782  u3lem8  783  u3lem10  785  u3lem11  786  u3lem13a  789  u3lem13b  790  u3lem14a  791  u3lem15  795  u3lemax4  796  bi1o1a  798  biao  799  i2i1i1  800  test2  803  3vth6  809  3vth9  812  3vded21  817  3vded22  818  1oa  820  2oalem1  825  2oath1  826  oale  829  sa5  836  salem1  837  sadm3  838  bi3  839  bi4  840  imp3  841  orbi  842  mlaconj4  844  negantlem10  861  neg3antlem2  865  comanblem1  870  comanblem2  871  mhlemlem1  874  mhlem  876  mhlem1  877  marsdenlem2  881  marsdenlem3  882  marsdenlem4  883  mlaconjolem  885  mlaconjo  886  mhcor1  888  e2astlem1  895  gomaex3lem6  919  gomaex3  924  oas  925  oa6v4v  933  oa4v3v  934  oal42  935  oa23  936  distoa  944  oa3to4lem6  950  oa6todual  952  oa6fromdual  953  oa6fromdualn  954  oa6to4  958  oa4to6  965  oa4dcom  970  oa8todual  971  oa8to5  972  oa4to4u  973  oa4uto4g  975  oa4gto4u  976  oa3-6lem  980  oa3-3lem  981  oa3-1lem  982  oa3-4lem  983  oa3-5lem  984  oa3-u1lem  985  oa3-u2lem  986  oa3-6to3  987  oa3-2to4  988  oa3-2to2s  990  oa3-u1  991  oa3-u2  992  d4oa  996  oal2  999  oal1  1000  oaliii  1001  oalem2  1006  mloa  1018  4oaiii  1040  lem3.3.7i5e1  1072  lem3.3.7i5e2  1073  lem3.4.6  1079  lem4.6.6i0j1  1088  lem4.6.6i0j2  1089  lem4.6.6i0j3  1090  lem4.6.6i0j4  1091  lem4.6.6i1j0  1092  lem4.6.6i1j3  1094  lem4.6.6i2j0  1095  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j0  1100  lem4.6.6i4j2  1101  wdcom  1105  vneulem13  1143  vneulemexp  1148  dp15lemc  1156  dp15lemd  1157  dp15leme  1158  dp15lemg  1160  dp41lemf  1188  dp41lemg  1189  dp41lemj  1191  dp41lemk  1192  dp41leml  1193  xdp41  1198  xdp15  1199  xxdp41  1201  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208