Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → 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: orci
864 olci
865 pm2.25
889 curryax
893 exmid
894 pm2.13
897 pm5.11g
943 pm5.12
945 pm5.14
946 pm5.55
948 pm3.12
993 pm5.15
1012 pm5.54
1017 4exmid
1051 rb-ax2
1756 rb-ax3
1757 rb-ax4
1758 exmo
2537 axi12
2702 exmidne
2951 ifeqor
4580 fvbr0
6921 letrii
11339 clwwlknondisj
29364 poimirlem26
36514 tsbi3
37003 tsan2
37010 tsan3
37011 clsk1indlem2
42793 |