Step |
Hyp |
Ref |
Expression |
1 |
|
ss2in |
|- ( ( C C_ A /\ D C_ B ) -> ( C i^i D ) C_ ( A i^i B ) ) |
2 |
1
|
3adant1 |
|- ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( C i^i D ) C_ ( A i^i B ) ) |
3 |
|
eqimss |
|- ( ( A i^i B ) = (/) -> ( A i^i B ) C_ (/) ) |
4 |
3
|
3ad2ant1 |
|- ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( A i^i B ) C_ (/) ) |
5 |
2 4
|
sstrd |
|- ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( C i^i D ) C_ (/) ) |
6 |
|
ss0 |
|- ( ( C i^i D ) C_ (/) -> ( C i^i D ) = (/) ) |
7 |
5 6
|
syl |
|- ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( C i^i D ) = (/) ) |