Theorem fucofulem1

Description: Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fucofulem1.1	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ) )
2		fucofulem1.2	⊢ ( ( 𝜑 ∧ ( 𝜃 ∧ 𝜏 ) ) → 𝜂 )
3		fucofulem1.3	⊢ 𝜒
4		fucofulem1.4	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜃 )
5		fucofulem1.5	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜏 )
6		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
7	1	biimpa	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) )
8	7	simp2d	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )
9	7	simp3d	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜏 )
10	6 8 9 2	syl12anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜂 )
11		simpl	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜑 )
12	3	a1i	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜒 )
13	1	biimpar	⊢ ( ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ) → 𝜓 )
14	11 12 4 5 13	syl13anc	⊢ ( ( 𝜑 ∧ 𝜂 ) → 𝜓 )
15	10 14	impbida	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜂 ) )