Theorem redundpbi1

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

	Ref	Expression
Hypothesis	redundpbi1.1	|- ( ph <-> th )
Assertion	redundpbi1	|- ( redund ( ph , ps , ch ) <-> redund ( th , ps , ch ) )

Proof

Step	Hyp	Ref	Expression
1		redundpbi1.1	|- ( ph <-> th )
2	1	imbi1i	|- ( ( ph -> ps ) <-> ( th -> ps ) )
3	1	anbi1i	|- ( ( ph /\ ch ) <-> ( th /\ ch ) )
4	3	bibi1i	|- ( ( ( ph /\ ch ) <-> ( ps /\ ch ) ) <-> ( ( th /\ ch ) <-> ( ps /\ ch ) ) )
5	2 4	anbi12i	|- ( ( ( ph -> ps ) /\ ( ( ph /\ ch ) <-> ( ps /\ ch ) ) ) <-> ( ( th -> ps ) /\ ( ( th /\ ch ) <-> ( ps /\ ch ) ) ) )
6		df-redundp	|- ( redund ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( ( ph /\ ch ) <-> ( ps /\ ch ) ) ) )
7		df-redundp	|- ( redund ( th , ps , ch ) <-> ( ( th -> ps ) /\ ( ( th /\ ch ) <-> ( ps /\ ch ) ) ) )
8	5 6 7	3bitr4i	|- ( redund ( ph , ps , ch ) <-> redund ( th , ps , ch ) )