Theorem redundpim3

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

	Ref	Expression
Hypothesis	redundpim3.1	⊢ ( 𝜃 → 𝜒 )
Assertion	redundpim3	⊢ ( redund ( 𝜑 , 𝜓 , 𝜒 ) → redund ( 𝜑 , 𝜓 , 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		redundpim3.1	⊢ ( 𝜃 → 𝜒 )
2		anbi1	⊢ ( ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) → ( ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜃 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) ) )
3	1	pm4.71ri	⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝜃 ) )
4	3	bianass	⊢ ( ( 𝜑 ∧ 𝜃 ) ↔ ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜃 ) )
5	3	bianass	⊢ ( ( 𝜓 ∧ 𝜃 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) )
6	2 4 5	3bitr4g	⊢ ( ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜑 ∧ 𝜃 ) ↔ ( 𝜓 ∧ 𝜃 ) ) )
7	6	anim2i	⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ↔ ( 𝜓 ∧ 𝜃 ) ) ) )
8		df-redundp	⊢ ( redund ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) ) ) )
9		df-redundp	⊢ ( redund ( 𝜑 , 𝜓 , 𝜃 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ( 𝜑 ∧ 𝜃 ) ↔ ( 𝜓 ∧ 𝜃 ) ) ) )
10	7 8 9	3imtr4i	⊢ ( redund ( 𝜑 , 𝜓 , 𝜒 ) → redund ( 𝜑 , 𝜓 , 𝜃 ) )