Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∨ wo 845 |
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 846 |
This theorem is referenced by: orbi2i
911 pm1.5
918 pm2.3
923 r19.44v
3193 elpwunsn
4687 elsuci
6431 infxpenlem
10007 fin1a2lem12
10405 fin1a2
10409 entri3
10553 zindd
12662 elfzr
13744 hashnn0pnf
14301 limccnp
25407 tgldimor
27750 ex-natded5.7-2
29662 chirredi
31642 meran1
35291 dissym1
35301 ordtoplem
35315 ordcmp
35327 poimirlem31
36514 simpcntrab
45576 setc2othin
47666 |