Theorem lor 70

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 38	. 2 (a v c) = (b v c)
3		ax-a2 31	. 2 (c v a) = (a v c)
4		ax-a2 31	. 2 (c v b) = (b v c)
5	2, 3, 4	3tr1 63	1 (c v a) = (c v b)

Syntax hints:   = wb 1   v wo 6

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  a5b 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  4oagen1 1041  lem3.3.3lem2 1049  lem3.3.3 1051  lem3.3.4 1052  lem3.3.6 1055  lem3.3.7i0e1 1056  lem3.3.7i1e1 1059  lem3.3.7i1e2 1060  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem4.6.2e1 1079  lem4.6.6i1j3 1091  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098  wdcom 1102  wdwom 1103

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

Copyright terms: Public domain