| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-tp |
|- { A , B , C } = ( { A , B } u. { C } ) |
| 2 |
1
|
ineq1i |
|- ( { A , B , C } i^i { D } ) = ( ( { A , B } u. { C } ) i^i { D } ) |
| 3 |
|
disjprsn |
|- ( ( A =/= D /\ B =/= D ) -> ( { A , B } i^i { D } ) = (/) ) |
| 4 |
3
|
3adant3 |
|- ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { A , B } i^i { D } ) = (/) ) |
| 5 |
|
disjsn2 |
|- ( C =/= D -> ( { C } i^i { D } ) = (/) ) |
| 6 |
5
|
3ad2ant3 |
|- ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { C } i^i { D } ) = (/) ) |
| 7 |
4 6
|
jca |
|- ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( ( { A , B } i^i { D } ) = (/) /\ ( { C } i^i { D } ) = (/) ) ) |
| 8 |
|
undisj1 |
|- ( ( ( { A , B } i^i { D } ) = (/) /\ ( { C } i^i { D } ) = (/) ) <-> ( ( { A , B } u. { C } ) i^i { D } ) = (/) ) |
| 9 |
7 8
|
sylib |
|- ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( ( { A , B } u. { C } ) i^i { D } ) = (/) ) |
| 10 |
2 9
|
eqtrid |
|- ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { A , B , C } i^i { D } ) = (/) ) |