Colors of
variables: term |
Syntax hints: ≤
wle 2 ∩ wa 7 |
This theorem was proved from axioms:
ax-a1 30 ax-a2 31 ax-a3 32
ax-a5 34 ax-r1 35 ax-r2 36
ax-r4 37 ax-r5 38 |
This theorem depends on definitions:
df-a 40 df-t 41 df-f 42
df-le1 130 df-le2 131 |
This theorem is referenced by: distlem
188 str
189 womao
220 womaon
221 womaa
222 womaan
223 anorabs2
224 mccune2
247 oaidlem1
294 nom14
311 id5leid0
351 k1-8a
355 2vwomlem
365 ska4
433 i3orlem7
558 ud3lem1a
566 ud4lem1b
578 ud5lem1b
587 bi1o1a
798 biao
799 i2i1i1
800 3vth2
805 3vth6
809 3vded21
817 oaeqv
830 mlaconj4
844 negantlem2
849 negantlem9
859 negantlem10
861 neg3antlem2
865 mhlem
876 mhlem2
878 mh
879 distid
887 oago3.21x
890 cancellem
891 govar2
897 gon2n
898 gomaex4
900 oas
925 oat
927 oau
929 oa23
936 oa4lem1
937 oa4lem2
938 oaliv
1003 oagen1
1014 oa3moa3
1029 4oaiii
1040 4oagen1
1042 lem3.3.3lem3
1051 lem3.3.7i4e1
1069 lem3.3.7i4e2
1070 lem3.3.7i5e1
1072 lem3.4.3
1076 com3iia
1102 lem4.6.7
1103 ml
1123 mldual2i
1127 ml3le
1129 vneulem1
1131 vneulem6
1136 vneulem7
1137 vneulem13
1143 vneulemexp
1148 dp53lema
1163 dp53lemc
1165 dp53lemd
1166 dp53lemf
1168 dp35lemd
1174 dp35lemc
1175 dp41lemh
1190 dp32
1196 xdp41
1198 xdp53
1200 xxdp41
1201 xxdp53
1203 xdp45lem
1204 xdp43lem
1205 xdp45
1206 xdp43
1207 3dp43
1208 oadp35lemc
1211 testmod2
1215 testmod2expanded
1216 |