redundpim3

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

		Ref	Expression
	Hypothesis	redundpim3.1	$⊢ θ \to χ$
	Assertion	redundpim3	$⊢ redund (φ, ψ, χ) \to redund (φ, ψ, θ)$

Step	Hyp	Ref	Expression
1		redundpim3.1	$⊢ θ \to χ$
2		anbi1	$⊢ ((φ \land χ) \leftrightarrow (ψ \land χ)) \to (((φ \land χ) \land θ) \leftrightarrow ((ψ \land χ) \land θ))$
3	1	pm4.71ri	$⊢ θ \leftrightarrow (χ \land θ)$
4	3	bianass	$⊢ (φ \land θ) \leftrightarrow ((φ \land χ) \land θ)$
5	3	bianass	$⊢ (ψ \land θ) \leftrightarrow ((ψ \land χ) \land θ)$
6	2 4 5	3bitr4g	$⊢ ((φ \land χ) \leftrightarrow (ψ \land χ)) \to ((φ \land θ) \leftrightarrow (ψ \land θ))$
7	6	anim2i	$⊢ ((φ \to ψ) \land ((φ \land χ) \leftrightarrow (ψ \land χ))) \to ((φ \to ψ) \land ((φ \land θ) \leftrightarrow (ψ \land θ)))$
8		df-redundp	$⊢ redund (φ, ψ, χ) \leftrightarrow ((φ \to ψ) \land ((φ \land χ) \leftrightarrow (ψ \land χ)))$
9		df-redundp	$⊢ redund (φ, ψ, θ) \leftrightarrow ((φ \to ψ) \land ((φ \land θ) \leftrightarrow (ψ \land θ)))$
10	7 8 9	3imtr4i	$⊢ redund (φ, ψ, χ) \to redund (φ, ψ, θ)$

Metamath Proof Explorer