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: orim2
789 orbi2d
790 pm2.82
812 stdcndcOLD
846 pm2.13dc
885 exmid1dc
4200 acexmidlemcase
5869 poxp
6232 fodjuomnilemdc
7141 omniwomnimkv
7164 exmidontriimlem1
7219 indpi
7340 suplocexprlemloc
7719 nneoor
9354 uzp1
9560 maxabslemlub
11215 xrmaxiflemlub
11255 exmidunben
12426 bj-nn0suc
14686 sbthomlem
14743 |