Theorem 0funcglem

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

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

Proof

Step	Hyp	Ref	Expression
1		0funcglem.1	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
2		0funcglem.2	|- ( ph -> ( ch <-> et ) )
3		0funcglem.3	|- ( ph -> ( th <-> ze ) )
4		0funcglem.4	|- ( ph -> ta )
5		df-3an	|- ( ( ch /\ th /\ ta ) <-> ( ( ch /\ th ) /\ ta ) )
6	1 5	bitrdi	|- ( ph -> ( ps <-> ( ( ch /\ th ) /\ ta ) ) )
7	4 6	mpbiran2d	|- ( ph -> ( ps <-> ( ch /\ th ) ) )
8	2 3	anbi12d	|- ( ph -> ( ( ch /\ th ) <-> ( et /\ ze ) ) )
9	7 8	bitrd	|- ( ph -> ( ps <-> ( et /\ ze ) ) )