Theorem lebi 145

Description: L.e. to biconditional.

Hypotheses

Ref	Expression
lebi.1	a =< b
lebi.2	b =< a

Assertion

Ref	Expression
lebi	a = b

Proof of Theorem lebi

Step	Hyp	Ref	Expression
1		lebi.2	. . . . 5 b =< a
2	1	df-le2 131	. . . 4 (b v a) = a
3	2	ax-r1 35	. . 3 a = (b v a)
4		ax-a2 31	. . 3 (b v a) = (a v b)
5	3, 4	ax-r2 36	. 2 a = (a v b)
6		lebi.1	. . 3 a =< b
7	6	df-le2 131	. 2 (a v b) = b
8	5, 7	ax-r2 36	1 a = b

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

This theorem is referenced by:  distlem 188  womao 220  womaon 221  womaa 222  womaan 223  anorabs2 224  ka4lemo 228  wlem1 243  mccune2 247  wql1lem 287  wql2lem 288  womle2a 295  nom14 311  go1 343  k1-8a 355  2vwomlem 365  wr5-2v 366  wdf-c2 384  ska2 432  ska4 433  ka4ot 435  ortha 438  cmtr1com 493  i3or 497  i3ri3 538  i3li3 539  i32i3 540  ud4lem1a 577  i2bi 722  u12lem 771  u3lemax4 796  u3lemax5 797  bi1o1a 798  biao 799  i2i1i1 800  3vth2 805  3vded11 814  3vded12 815  1oaiii 823  3vroa 831  negant 852  negant3 860  negant4 862  neg3ant1 866  mhlem 876  mh 879  distid 887  oago3.21x 890  cancel 892  gomaex4 900  gomaex3lem2 915  oau 929  oa23 936  oaliii 1001  oagen1 1014  oadist 1019  oadistb 1020  oadistc0 1021  oadistc 1022  oadistd 1023  4oaiii 1039  4oagen1 1041  4oadist 1043  lem3.3.5lem 1053  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071  lem4.6.6i0j1 1085  lem4.6.6i0j2 1086  lem4.6.6i0j3 1087  lem4.6.6i0j4 1088  lem4.6.6i2j1 1093  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098  com3iia 1099  lem4.6.7 1100  wdwom 1103

This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36

This theorem depends on definitions:  df-le2 131

Copyright terms: Public domain