Theorem 2or 67

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 66	. 2 (a v c) = (a v d)
3		2or.1	. . 3 a = b
4	3	ax-r5 37	. 2 (a v d) = (b v d)
5	2, 4	ax-r2 35	1 (a v c) = (b v d)

Syntax hints:   = wb 1   v wo 6

This theorem is referenced by:  oran 79  dfb 86  bicom 88  lbi 89  biid 108  1b 109  mi 117  omlem1 119  omlem2 120  ledir 167  comm0 170  comm1 171  bctr 173  cbtr 174  cmtrcom 182  wlem3.1 202  wwfh1 208  wwfh3 210  wwfh4 211  ka4lem 221  lei3 238  mccune2 239  i3n1 241  i3id 243  li3 244  ri3 245  ud1lem0b 248  ud2lem0a 250  ud4lem0a 254  ud4lem0b 255  ud5lem0a 256  ud5lem0b 257  i3i4 262  i5con 264  1i1 266  womle2a 287  nomcon2 295  nom15 304  nom24 309  nom25 310  nom40 317  nom51 324  nom53 326  2vwomr2 344  wdf-c2 366  wcom2or 409  ska2 414  ska4 415  wom2 416  ka4ot 417  woml6 418  woml7 419  lem3.1 425  comcom 435  comcom5 440  comdr 448  df2c1 450  fh1 451  fh1r 455  fh2r 456  com2or 465  oml4 469  gsth 471  comcmtr1 476  i3bi 478  dfi3b 481  dfi4b 482  i3n2 483  i3lem1 486  i3lem3 488  lem4 493  i3abs1 504  i3abs3 506  i3con 533  ud1lem1 542  ud1lem3 544  ud2lem1 545  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem1 552  ud3lem2 553  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem2 564  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1 571  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  ud5lem3 576  u1lemaa 582  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u2lemana 588  u3lemana 589  u4lemana 590  u5lemana 591  u3lemab 594  u4lemab 595  u5lemab 596  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u3lemob 614  u3lemonb 619  u3lemnana 629  u5lemnana 631  u4lemnab 635  u5lemnab 636  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u1lemnonb 657  u3lemnonb 659  u4lemnonb 660  u5lemnonb 661  u3lemc4 685  u4lemc4 686  i1com 690  u1lemle2 697  u4lemle2 700  u5lemle2 701  u5lembi 707  u12lembi 708  u21lembi 709  u1lemn1b 712  oi3oa3lem1 714  u4lem1 719  u3lem1n 723  u4lem1n 724  u5lem1n 725  u1lem2 726  u1lem3 731  u3lem3 733  u4lem3 734  u5lem3 735  u3lem3n 736  u4lem3n 737  u5lem3n 738  u4lem4 741  u4lem5 746  u4lem6 750  u24lem 752  u12lem 753  u2lem7 755  u3lem7 756  u2lem7n 757  u1lem8 758  u1lem11 762  u2lem8 764  u3lem8 765  u3lem10 767  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem14a 773  u3lem15 777  u3lemax4 778  bi1o1a 780  biao 781  i2i1i1 782  test2 785  3vth6 791  3vth9 794  3vded21 799  3vded22 800  1oa 802  2oalem1 807  2oath1 808  oale 811  sa5 818  salem1 819  sadm3 820  bi3 821  bi4 822  imp3 823  orbi 824  mlaconj4 826  negantlem10 843  neg3antlem2 847  comanblem1 852  comanblem2 853  mhlemlem1 856  mhlem 858  mhlem1 859  marsdenlem2 863  marsdenlem3 864  marsdenlem4 865  mlaconjolem 867  mlaconjo 868  mhcor1 870  gomaex3lem6 899  gomaex3 904  oas 905  oa6v4v 913  oa4v3v 914  oal42 915  oa23 916  distoa 924  oa3to4lem6 930  oa6todual 932  oa6fromdual 933  oa6fromdualn 934  oa6to4 938  oa4to6 945  oa4dcom 950  oa8todual 951  oa8to5 952  oa4to4u 953  oa4uto4g 955  oa4gto4u 956  oa3-6lem 960  oa3-3lem 961  oa3-1lem 962  oa3-4lem 963  oa3-5lem 964  oa3-u1lem 965  oa3-u2lem 966  oa3-6to3 967  oa3-2to4 968  oa3-2to2s 970  oa3-u1 971  oa3-u2 972  d4oa 976  oal2 979  oal1 980  oaliii 981  oalem2 986  mloa 998  4oaiii 1019

This theorem was proved from axioms:  ax-a2 30  ax-r1 34  ax-r2 35  ax-r5 37

metamath.org