Theorem 2or 72

Description: Join both sides with disjunction.

Hypotheses

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

Assertion

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

Proof of Theorem 2or

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

Syntax hints:   = wb 1   v wo 6

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 1039  lem3.3.7i5e1 1071  lem3.3.7i5e2 1072  lem3.4.6 1078  lem4.6.6i0j1 1085  lem4.6.6i0j2 1086  lem4.6.6i0j3 1087  lem4.6.6i0j4 1088  lem4.6.6i1j0 1089  lem4.6.6i1j3 1091  lem4.6.6i2j0 1092  lem4.6.6i2j1 1093  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j0 1097  lem4.6.6i4j2 1098  wdcom 1102

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

Copyright terms: Public domain