Definition df-redundp

Description: Define the redundancy operator for propositions, cf. df-redund . (Contributed by Peter Mazsa, 23-Oct-2022)

	Ref	Expression
Assertion	df-redundp	|- ( redund ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( ( ph /\ ch ) <-> ( ps /\ ch ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2		wch	|- ch
3	0 1 2	wredundp	|- redund ( ph , ps , ch )
4	0 1	wi	|- ( ph -> ps )
5	0 2	wa	|- ( ph /\ ch )
6	1 2	wa	|- ( ps /\ ch )
7	5 6	wb	|- ( ( ph /\ ch ) <-> ( ps /\ ch ) )
8	4 7	wa	|- ( ( ph -> ps ) /\ ( ( ph /\ ch ) <-> ( ps /\ ch ) ) )
9	3 8	wb	|- ( redund ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( ( ph /\ ch ) <-> ( ps /\ ch ) ) ) )