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
3191 elpwunsn
4649 elsuci
6389 infxpenlem
9956 fin1a2lem12
10354 fin1a2
10358 entri3
10502 zindd
12611 elfzr
13692 hashnn0pnf
14249 limccnp
25271 tgldimor
27486 ex-natded5.7-2
29398 chirredi
31378 meran1
34912 dissym1
34922 ordtoplem
34936 ordcmp
34948 poimirlem31
36138 simpcntrab
45185 setc2othin
47150 |