Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ∨ wo 708 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 |
This theorem depends on definitions:
df-bi 117 |
This theorem is referenced by: orbi2i
762 pm1.5
765 pm2.3
775 ordi
816 dcn
842 pm2.25dc
893 dcan
933 axi12
1514 dveeq2or
1816 equs5or
1830 sb4or
1833 sb4bor
1835 nfsb2or
1837 sbequilem
1838 sbequi
1839 sbal1yz
2001 dvelimor
2018 exmodc
2076 r19.44av
2636 exmidundif
4207 exmidundifim
4208 exmid1stab
4209 elsuci
4404 acexmidlemcase
5870 undifdcss
6922 updjudhf
7078 ctssdccl
7110 zindd
9371 fiubm
10808 fsumsplitsn
11418 fprodcllem
11614 fprodsplitsn
11641 subctctexmid
14753 |