Theorem bile 142

Description: Biconditional to "less than or equal to". (Contributed by NM, 27-Aug-1997.)

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 ∪ b) = (b ∪ b)
3		oridm 110	. . 3 (b ∪ b) = b
4	2, 3	ax-r2 36	. 2 (a ∪ b) = b
5	4	df-le1 130	1 a ≤ b

Syntax hints:   = wb 1   ≤ wle 2   ∪ wo 6

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

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  dp15lemf  1159  dp35leme  1173  dp35lemd  1174  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208