Metamath Proof Explorer


Theorem redundeq1

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

Ref Expression
Hypothesis redundeq1.1 A = D
Assertion redundeq1 A Redund B C D Redund B C

Proof

Step Hyp Ref Expression
1 redundeq1.1 A = D
2 1 sseq1i A B D B
3 1 ineq1i A C = D C
4 3 eqeq1i A C = B C D C = B C
5 2 4 anbi12i A B A C = B C D B D C = B C
6 df-redund A Redund B C A B A C = B C
7 df-redund D Redund B C D B D C = B C
8 5 6 7 3bitr4i A Redund B C D Redund B C