lebi - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > lebi		Unicode version

Theorem lebi 145

Description: L.e. to biconditional.

**Hypotheses**
Ref	Expression
lebi.1
lebi.2

**Assertion**
Ref	Expression
lebi

**Proof of Theorem lebi**
Step	Hyp	Ref	Expression
1		lebi.2	. . . . 5
2	1	df-le2 131	. . . 4
3	2	ax-r1 35	. . 3
4		ax-a2 31	. . 3
5	3, 4	ax-r2 36	. 2
6		lebi.1	. . 3
7	6	df-le2 131	. 2
8	5, 7	ax-r2 36	1

Colors of variables: term

Syntax hints:

wb 1

wle 2

wo 6

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

This theorem depends on definitions: df-le2 131

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 1040 4oagen1 1042 4oadist 1044 lem3.3.5lem 1054 lem3.3.7i4e1 1069 lem3.3.7i4e2 1070 lem3.3.7i5e1 1072 lem4.6.6i0j1 1086 lem4.6.6i0j2 1087 lem4.6.6i0j3 1088 lem4.6.6i0j4 1089 lem4.6.6i2j1 1094 lem4.6.6i2j4 1095 lem4.6.6i3j0 1096 lem4.6.6i3j1 1097 lem4.6.6i4j2 1099 com3iia 1100 lem4.6.7 1101 wdwom 1104 ml 1121 mldual2i 1125 ml3 1128 vneulem1 1129 vneulem6 1134 vneulem7 1135 vneulem13 1141 vneulemexp 1146