Theorem redundpbi1

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

	Ref	Expression
Hypothesis	redundpbi1.1	⊢ ( 𝜑 ↔ 𝜃 )
Assertion	redundpbi1	⊢ ( redund ( 𝜑 , 𝜓 , 𝜒 ) ↔ redund ( 𝜃 , 𝜓 , 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		redundpbi1.1	⊢ ( 𝜑 ↔ 𝜃 )
2	1	imbi1i	⊢ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜃 → 𝜓 ) )
3	1	anbi1i	⊢ ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜃 ∧ 𝜒 ) )
4	3	bibi1i	⊢ ( ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜃 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) )
5	2 4	anbi12i	⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) ) ↔ ( ( 𝜃 → 𝜓 ) ∧ ( ( 𝜃 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) ) )
6		df-redundp	⊢ ( redund ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) ) )
7		df-redundp	⊢ ( redund ( 𝜃 , 𝜓 , 𝜒 ) ↔ ( ( 𝜃 → 𝜓 ) ∧ ( ( 𝜃 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) ) )
8	5 6 7	3bitr4i	⊢ ( redund ( 𝜑 , 𝜓 , 𝜒 ) ↔ redund ( 𝜃 , 𝜓 , 𝜒 ) )