Step |
Hyp |
Ref |
Expression |
1 |
|
redundss3.1 |
|- D C_ C |
2 |
|
ineq1 |
|- ( ( A i^i C ) = ( B i^i C ) -> ( ( A i^i C ) i^i D ) = ( ( B i^i C ) i^i D ) ) |
3 |
|
dfss |
|- ( D C_ C <-> D = ( D i^i C ) ) |
4 |
1 3
|
mpbi |
|- D = ( D i^i C ) |
5 |
|
incom |
|- ( D i^i C ) = ( C i^i D ) |
6 |
4 5
|
eqtri |
|- D = ( C i^i D ) |
7 |
6
|
ineq2i |
|- ( A i^i D ) = ( A i^i ( C i^i D ) ) |
8 |
|
inass |
|- ( ( A i^i C ) i^i D ) = ( A i^i ( C i^i D ) ) |
9 |
7 8
|
eqtr4i |
|- ( A i^i D ) = ( ( A i^i C ) i^i D ) |
10 |
6
|
ineq2i |
|- ( B i^i D ) = ( B i^i ( C i^i D ) ) |
11 |
|
inass |
|- ( ( B i^i C ) i^i D ) = ( B i^i ( C i^i D ) ) |
12 |
10 11
|
eqtr4i |
|- ( B i^i D ) = ( ( B i^i C ) i^i D ) |
13 |
2 9 12
|
3eqtr4g |
|- ( ( A i^i C ) = ( B i^i C ) -> ( A i^i D ) = ( B i^i D ) ) |
14 |
13
|
anim2i |
|- ( ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) -> ( A C_ B /\ ( A i^i D ) = ( B i^i D ) ) ) |
15 |
|
df-redund |
|- ( A Redund <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) ) |
16 |
|
df-redund |
|- ( A Redund <. B , D >. <-> ( A C_ B /\ ( A i^i D ) = ( B i^i D ) ) ) |
17 |
14 15 16
|
3imtr4i |
|- ( A Redund <. B , C >. -> A Redund <. B , D >. ) |