Theorem 0funcglem

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

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

Proof

Step	Hyp	Ref	Expression
1		0funcglem.1	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ) )
2		0funcglem.2	⊢ ( 𝜑 → ( 𝜒 ↔ 𝜂 ) )
3		0funcglem.3	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜁 ) )
4		0funcglem.4	⊢ ( 𝜑 → 𝜏 )
5		df-3an	⊢ ( ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ↔ ( ( 𝜒 ∧ 𝜃 ) ∧ 𝜏 ) )
6	1 5	bitrdi	⊢ ( 𝜑 → ( 𝜓 ↔ ( ( 𝜒 ∧ 𝜃 ) ∧ 𝜏 ) ) )
7	4 6	mpbiran2d	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ) ) )
8	2 3	anbi12d	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜃 ) ↔ ( 𝜂 ∧ 𝜁 ) ) )
9	7 8	bitrd	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜂 ∧ 𝜁 ) ) )