Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → 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: orci
863 olci
864 pm2.25
888 curryax
892 exmid
893 pm2.13
896 pm5.11g
942 pm5.12
944 pm5.14
945 pm5.55
947 pm3.12
992 pm5.15
1011 pm5.54
1016 4exmid
1050 rb-ax2
1755 rb-ax3
1756 rb-ax4
1757 exmo
2536 axi12
2701 exmidne
2950 ifeqor
4579 fvbr0
6920 letrii
11338 clwwlknondisj
29361 poimirlem26
36509 tsbi3
36998 tsan2
37005 tsan3
37006 clsk1indlem2
42783 |