Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∨ wo 846 |
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 206 df-or 847 |
This theorem is referenced by: orbi2i
912 pm1.5
919 pm2.3
924 r19.44v
3194 elpwunsn
4688 elsuci
6432 infxpenlem
10008 fin1a2lem12
10406 fin1a2
10410 entri3
10554 zindd
12663 elfzr
13745 hashnn0pnf
14302 limccnp
25408 tgldimor
27784 ex-natded5.7-2
29696 chirredi
31678 meran1
35344 dissym1
35354 ordtoplem
35368 ordcmp
35380 poimirlem31
36567 simpcntrab
45634 setc2othin
47724 |