Theorem redundpim3

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

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

Proof

Step	Hyp	Ref	Expression
1		redundpim3.1	|- ( th -> ch )
2		anbi1	|- ( ( ( ph /\ ch ) <-> ( ps /\ ch ) ) -> ( ( ( ph /\ ch ) /\ th ) <-> ( ( ps /\ ch ) /\ th ) ) )
3	1	pm4.71ri	|- ( th <-> ( ch /\ th ) )
4	3	bianass	|- ( ( ph /\ th ) <-> ( ( ph /\ ch ) /\ th ) )
5	3	bianass	|- ( ( ps /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
6	2 4 5	3bitr4g	|- ( ( ( ph /\ ch ) <-> ( ps /\ ch ) ) -> ( ( ph /\ th ) <-> ( ps /\ th ) ) )
7	6	anim2i	|- ( ( ( ph -> ps ) /\ ( ( ph /\ ch ) <-> ( ps /\ ch ) ) ) -> ( ( ph -> ps ) /\ ( ( ph /\ th ) <-> ( ps /\ th ) ) ) )
8		df-redundp	|- ( redund ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( ( ph /\ ch ) <-> ( ps /\ ch ) ) ) )
9		df-redundp	|- ( redund ( ph , ps , th ) <-> ( ( ph -> ps ) /\ ( ( ph /\ th ) <-> ( ps /\ th ) ) ) )
10	7 8 9	3imtr4i	|- ( redund ( ph , ps , ch ) -> redund ( ph , ps , th ) )