Theorem 0funclem

Description: Lemma for 0funcALT . (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	0funclem.1	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
	0funclem.2	|- ( ch <-> et )
	0funclem.3	|- ( th <-> ze )
	0funclem.4	|- ta
Assertion	0funclem	|- ( ph -> ( ps <-> ( et /\ ze ) ) )

Proof

Step	Hyp	Ref	Expression
1		0funclem.1	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
2		0funclem.2	|- ( ch <-> et )
3		0funclem.3	|- ( th <-> ze )
4		0funclem.4	|- ta
5		df-3an	|- ( ( ch /\ th /\ ta ) <-> ( ( ch /\ th ) /\ ta ) )
6	1 5	bitrdi	|- ( ph -> ( ps <-> ( ( ch /\ th ) /\ ta ) ) )
7	6	rbaibd	|- ( ( ph /\ ta ) -> ( ps <-> ( ch /\ th ) ) )
8	4 7	mpan2	|- ( ph -> ( ps <-> ( ch /\ th ) ) )
9	2 3	anbi12i	|- ( ( ch /\ th ) <-> ( et /\ ze ) )
10	8 9	bitrdi	|- ( ph -> ( ps <-> ( et /\ ze ) ) )