Theorem lel2or 170

Description: Disjunction of 2 l.e.'s

Hypotheses

Ref	Expression
lel2.1	a =< b
lel2.2	c =< b

Assertion

Ref	Expression
lel2or	(a v c) =< b

Proof of Theorem lel2or

Step	Hyp	Ref	Expression
1		lel2.1	. . 3 a =< b
2		lel2.2	. . 3 c =< b
3	1, 2	le2or 168	. 2 (a v c) =< (b v b)
4		oridm 110	. 2 (b v b) = b
5	3, 4	lbtr 139	1 (a v c) =< b

Syntax hints:   =< wle 2   v wo 6

This theorem is referenced by:  womao 220  womaon 221  womaa 222  womaan 223  anorabs2 224  mccune2 247  nom14 311  i2or 344  i1or 345  i5lei1 347  i5lei2 348  k1-2 357  k1-3 358  wdf-c2 384  cmtr1com 493  i0cmtrcom 495  ud3lem1c 568  ud3lem3 576  ud4lem1c 579  ud4lem1 581  ud5lem1 589  u3lemana 607  u4lemab 613  u5lemab 614  u3lemona 627  u4lemona 628  u5lemona 629  u4lemob 633  u5lemob 634  i2bi 722  u4lem1 737  u4lem5 764  u4lem6 768  u12lem 771  u3lem13a 789  u3lem13b 790  3vded11 814  3vded12 815  3vded22 818  1oa 820  mlalem 832  sa5 836  sadm3 838  negantlem2 849  negantlem4 851  negantlem9 859  negantlem10 861  neg3antlem2 865  neg3ant1 866  mhlem2 878  mh 879  cancellem 891  kb10iii 893  gomaex3lem2 915  oas 925  oatr 928  oaur 930  oal42 935  oa3to4lem4 948  oa4b 959  oa4to4u2 974  oa3-u1lem 985  oa3-u1 991  oa3-u2 992  oa3-1to5 993  d4oa 996  oadist2b 1008  mloa 1018  lem3.3.7i4e1 1068  lem4.6.6i0j1 1085  lem4.6.6i0j2 1086  lem4.6.6i0j3 1087  lem4.6.6i0j4 1088  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  lem4.6.7 1100

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