Theorem bile 134

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 37	. . 3 (a ∪ b) = (b ∪ b)
3		oridm 102	. . 3 (b ∪ b) = b
4	2, 3	ax-r2 35	. 2 (a ∪ b) = b
5	4	df-le1 122	1 a ≤ b

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

This theorem is referenced by:  qlhoml1a 135  qlhoml1b 136  leid 140  str 181  mccune2 239  wom3 349  i3ri3 520  i3li3 521  i32i3 522  u12lem 753  sadm3 820  mlaconj4 826  mlaconjo 868  oaidlem2 911  oaidlem2g 912  distoah1 920  d3oa 975  oadist2 989  mloa 998  oadist 999

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

This theorem depends on definitions:  df-t 40  df-f 41  df-le1 122

metamath.org