Theorem 0funclem

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

	Ref	Expression
Hypotheses	0funclem.1	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ) )
	0funclem.2	⊢ ( 𝜒 ↔ 𝜂 )
	0funclem.3	⊢ ( 𝜃 ↔ 𝜁 )
	0funclem.4	⊢ 𝜏
Assertion	0funclem	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜂 ∧ 𝜁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		0funclem.1	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ) )
2		0funclem.2	⊢ ( 𝜒 ↔ 𝜂 )
3		0funclem.3	⊢ ( 𝜃 ↔ 𝜁 )
4		0funclem.4	⊢ 𝜏
5		df-3an	⊢ ( ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ↔ ( ( 𝜒 ∧ 𝜃 ) ∧ 𝜏 ) )
6	1 5	bitrdi	⊢ ( 𝜑 → ( 𝜓 ↔ ( ( 𝜒 ∧ 𝜃 ) ∧ 𝜏 ) ) )
7	6	rbaibd	⊢ ( ( 𝜑 ∧ 𝜏 ) → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ) ) )
8	4 7	mpan2	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ) ) )
9	2 3	anbi12i	⊢ ( ( 𝜒 ∧ 𝜃 ) ↔ ( 𝜂 ∧ 𝜁 ) )
10	8 9	bitrdi	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜂 ∧ 𝜁 ) ) )