Colors of
variables: wff setvar class |
Syntax hints: →
wi 4 ↔ wb 176 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 |
This theorem depends on definitions:
df-bi 177 |
This theorem is referenced by: impbid2
195 iba
489 ibar
490 pm5.71
902 cad0
1400 19.33b
1608 19.9t
1779 19.9tOLD
1857 a16gb
2050 sb4b
2054 eupickbi
2270 euor2
2272 2eu1
2284 2eu3
2286 ceqsalg
2884 undif4
3608 sneqbg
3876 adj11
3890 elpwuni
4054 opkthg
4132 iotanul
4355 preaddccan2
4456 suc11nnc
4559 phialllem1
4617 ssxpb
5056 xp11
5057 xpcan
5058 xpcan2
5059 imadif
5172 2elresin
5195 f1fveq
5474 f1elima
5475 enpw1
6063 peano4nc
6151 addceq0
6220 ce0tb
6239 addccan2nc
6266 |