Colors of
variables: wff setvar class |
Syntax hints: wn 3
wi 4
wo 357 |
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 177 df-or 359 |
This theorem is referenced by: jaod
369 pm1.4
375 jaoa
496 pm1.2
499 orim12i
502 pm1.5
508 pm2.41
556 pm2.42
557 pm2.4
558 pm4.44
560 jaoian
759 pm2.64
764 pm2.82
825 pm3.2ni
827 andi
837 ecase3
907 consensus
925 cad1
1398 19.33
1607 19.33b
1608 dfsb2
2055 mooran1
2258 2eu3
2286 eueq3
3012 sbcor
3091 elun
3221 sspss
3369 sspsstr
3375 ssun
3443 inss
3485 undif3
3516 ifbi
3680 elpr2
3753 pwpw0
3856 sssn
3865 snsssn
3874 pwsnALT
3883 unissint
3951 pwadjoin
4120 preq12b
4128 abexv
4325 nnc0suc
4413 lefinlteq
4464 ltfintri
4467 clos1basesuc
5883 nchoicelem17
6306 |