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 ∪ 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  1157  dp35leme  1171  dp35lemd  1172  xdp15  1197  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206