Metamath Proof Explorer


Theorem redundss3

Description: Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022)

Ref Expression
Hypothesis redundss3.1 D C
Assertion redundss3 A Redund B C A Redund B D

Proof

Step Hyp Ref Expression
1 redundss3.1 D C
2 ineq1 A C = B C A C D = B C D
3 dfss D C D = D C
4 1 3 mpbi D = D C
5 incom D C = C D
6 4 5 eqtri D = C D
7 6 ineq2i A D = A C D
8 inass A C D = A C D
9 7 8 eqtr4i A D = A C D
10 6 ineq2i B D = B C D
11 inass B C D = B C D
12 10 11 eqtr4i B D = B C D
13 2 9 12 3eqtr4g A C = B C A D = B D
14 13 anim2i A B A C = B C A B A D = B D
15 df-redund A Redund B C A B A C = B C
16 df-redund A Redund B D A B A D = B D
17 14 15 16 3imtr4i A Redund B C A Redund B D