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
4206 exmidundifim
4207 exmid1stab
4208 elsuci
4403 acexmidlemcase
5869 undifdcss
6921 updjudhf
7077 ctssdccl
7109 zindd
9370 fiubm
10807 fsumsplitsn
11417 fprodcllem
11613 fprodsplitsn
11640 subctctexmid
14720 |