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
4201 acexmidlemcase
5870 poxp
6233 fodjuomnilemdc
7142 omniwomnimkv
7165 exmidontriimlem1
7220 indpi
7341 suplocexprlemloc
7720 nneoor
9355 uzp1
9561 maxabslemlub
11216 xrmaxiflemlub
11256 exmidunben
12427 bj-nn0suc
14719 sbthomlem
14776 |