Step |
Hyp |
Ref |
Expression |
1 |
|
soi.1 |
|- R Or S |
2 |
|
soi.2 |
|- R C_ ( S X. S ) |
3 |
2
|
brel |
|- ( A R B -> ( A e. S /\ B e. S ) ) |
4 |
3
|
simpld |
|- ( A R B -> A e. S ) |
5 |
2
|
brel |
|- ( B R C -> ( B e. S /\ C e. S ) ) |
6 |
4 5
|
anim12i |
|- ( ( A R B /\ B R C ) -> ( A e. S /\ ( B e. S /\ C e. S ) ) ) |
7 |
|
sotr |
|- ( ( R Or S /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( ( A R B /\ B R C ) -> A R C ) ) |
8 |
1 7
|
mpan |
|- ( ( A e. S /\ B e. S /\ C e. S ) -> ( ( A R B /\ B R C ) -> A R C ) ) |
9 |
8
|
3expb |
|- ( ( A e. S /\ ( B e. S /\ C e. S ) ) -> ( ( A R B /\ B R C ) -> A R C ) ) |
10 |
6 9
|
mpcom |
|- ( ( A R B /\ B R C ) -> A R C ) |