Theorem bile 142

Description: Biconditional to l.e.

Hypothesis

Ref	Expression
bile.1	a = b

Assertion

Ref	Expression
bile	a =< b

Proof of Theorem bile

Step	Hyp	Ref	Expression
1		bile.1	. . . 4 a = b
2	1	ax-r5 38	. . 3 (a v b) = (b v b)
3		oridm 110	. . 3 (b v b) = b
4	2, 3	ax-r2 36	. 2 (a v b) = b
5	4	df-le1 130	1 a =< b

Syntax hints:   = wb 1   =< wle 2   v wo 6

This theorem is referenced by:  qlhoml1a 143  qlhoml1b 144  leid 148  str 189  mccune2 247  wom3 367  i3ri3 538  i3li3 539  i32i3 540  u12lem 771  sadm3 838  mlaconj4 844  mlaconjo 886  oaidlem2 931  oaidlem2g 932  distoah1 940  d3oa 995  oadist2 1009  mloa 1018  oadist 1019  dplem15f 1153

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

This theorem depends on definitions:  df-t 41  df-f 42  df-le1 130

Copyright terms: Public domain