Theorem lor 66

Description: Inference introducing disjunct to left.

Hypothesis

Ref	Expression
lor.1	a = b

Assertion

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

Proof of Theorem lor

Step	Hyp	Ref	Expression
1		lor.1	. . 3 a = b
2	1	ax-r5 37	. 2 (a v c) = (b v c)
3		ax-a2 30	. 2 (c v a) = (a v c)
4		ax-a2 30	. 2 (c v b) = (b v c)
5	2, 3, 4	3tr1 60	1 (c v a) = (c v b)

Syntax hints:   = wb 1   v wo 6

This theorem is referenced by:  2or 67  anass 69  lan 70  or32 75  or4 77  anor1 80  or0 94  or1 96  an1 98  an0 100  oridm 102  orordir 105  a5b 112  conb 114  leao 116  di 118  wwoml2 204  wwoml3 205  ka4lemo 220  sklem 222  ska3 224  lei3 238  mccune2 239  ni31 242  li3 244  ud1lem0a 247  ud2lem0b 251  ud4lem0a 254  i1i2 258  0i1 265  i1id 267  i2id 268  ud1lem0c 269  wql2lem2 281  wql2lem3 282  wql2lem5 284  wql1 285  oaidlem1 286  womle2a 287  nomb41 291  nomb32 292  nomcon1 294  nomcon2 295  nom11 300  nom12 301  nom13 302  nom14 303  nom21 306  nom22 307  nom23 308  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  2vwomr2 344  2vwomlem 347  wr5-2v 348  ska2 414  ska4 415  ka4ot 417  woml6 418  lem3a.1 426  omln 428  omla 429  oml5 431  oml5a 432  oml2 433  oml3 434  comcom 435  com3i 449  fh3 453  fh4 454  fh4c 460  gsth 471  gsth2 472  i0cmtrcom 477  i3bi 478  df2i3 480  dfi4b 482  i3n2 483  oi3ai3 485  i3lem3 488  lem4 493  i3abs1 504  i3th1 525  i3con 533  ud1lem1 542  ud1lem3 544  ud2lem1 545  ud2lem2 546  ud2lem3 547  ud3lem1c 550  ud3lem1 552  ud3lem2 553  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1c 561  ud4lem1 563  ud4lem2 564  ud4lem3b 566  ud4lem3 567  ud5lem1a 568  ud5lem1 571  ud5lem3a 573  ud5lem3 576  u1lemanb 597  u1lemoa 602  u2lemoa 603  u3lemoa 604  u4lemoa 605  u5lemoa 606  u4lemona 610  u5lemona 611  u2lemob 613  u3lemob 614  u4lemob 615  u1lemonb 617  u2lemonb 618  u3lemonb 619  u4lemonb 620  u5lemonb 621  u1lemnaa 622  u3lemnana 629  u5lemnana 631  u3lemc4 685  u4lemc4 686  u1lembi 702  u2lembi 703  i2bi 704  u1lem3var1 713  oi3oa3 715  u2lem1 717  u4lem1 719  u2lem2 727  u1lem3 731  u3lem3n 736  u4lem3n 737  u5lem3n 738  u1lem4 739  u4lem4 741  u5lem4 742  u1lem5 743  u2lem5 744  u4lem5 746  u3lem6 749  u4lem6 750  u24lem 752  u12lem 753  u1lem7 754  u2lem7 755  u3lem7 756  u1lem11 762  u3lem8 765  u3lem9 766  u3lem10 767  u3lem11 768  u3lem11a 769  u3lem13a 771  u3lem13b 772  u3lemax4 778  u3lemax5 779  bi1o1a 780  i2i1i1 782  i1abs 783  test 784  test2 785  3vth1 786  3vth4 789  3vth5 790  3vth6 791  3vth7 792  3vth9 794  3vded11 796  3vded21 799  3vded3 801  1oaii 806  2oalem1 807  2oath1 808  3vroa 813  orbi 824  mlaconj4 826  i1orni1 829  negant2 840  negantlem10 843  neg3antlem2 847  elimconslem 849  elimcons 850  elimcons2 851  comanblem1 852  comanb 854  mhlemlem2 857  mhlem 858  mhlem1 859  mh 861  mlaconjolem 867  mlaconjo 868  cancellem 873  govar 876  gomaex3lem1 894  oaidlem2 911  oaidlem2g 912  oa6v4v 913  oa4v3v 914  oa3to4lem1 925  oa3to4lem2 926  oa3to4lem5 929  oa3to4lem6 930  oa6to4 938  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa8to5 952  oa4to4u 953  oa4uto4g 955  oa3-2lema 958  oa3-2lemb 959  oa3-6lem 960  oa3-3lem 961  oa3-1lem 962  oa3-4lem 963  oa3-5lem 964  oa3-u1lem 965  oa3-u2lem 966  oa3-2to2s 970  oalii 982  oaliv 983  oalem2 986  oagen1 994  oadistc 1002  4oagen1 1021

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

metamath.org