Theorem lelor 166

Description: Add disjunct to left of both sides

Hypothesis

Ref	Expression
lel.1	a =< b

Assertion

Ref	Expression
lelor	(c v a) =< (c v b)

Proof of Theorem lelor

Step	Hyp	Ref	Expression
1		lel.1	. . 3 a =< b
2	1	leror 152	. 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	le3tr1 140	1 (c v a) =< (c v b)

Syntax hints:   =< wle 2   v wo 6

This theorem is referenced by:  le2or 168  ka4lemo 228  wlem1 243  wql1lem 287  nom14 311  nom20 313  nom21 314  nom22 315  go1 343  i2or 344  i1or 345  i5lei4 350  k1-8a 355  2vwomlem 365  wr5-2v 366  wdf-c2 384  ska2 432  ska4 433  i3or 497  i3orlem3 554  i2bi 722  u12lem 771  u3lem14mp 794  u3lemax4 796  u3lemax5 797  test2 803  3vded11 814  3vded22 818  sadm3 838  elimconslem 867  elimcons 868  govar2 897  oas 925  oat 927  oau 929  oa23 936  oa4lem1 937  oa4lem2 938  oa3to4lem1 945  oa3to4lem2 946  oa3to4lem3 947  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oa4to6lem4 963  oa4btoc 966  oa4uto4g 975  oa4uto4 977  oalem1 1005  mloa 1018  oadistc0 1021  lem3.3.5 1054  lem3.4.3 1075  lem4.6.6i0j1 1085  lem4.6.6i1j0 1089  lem4.6.6i1j3 1091  lem4.6.6i2j1 1093

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

Copyright terms: Public domain