Theorem fucofulem1

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

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

Proof

Step	Hyp	Ref	Expression
1		fucofulem1.1	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
2		fucofulem1.2	|- ( ( ph /\ ( th /\ ta ) ) -> et )
3		fucofulem1.3	|- ch
4		fucofulem1.4	|- ( ( ph /\ et ) -> th )
5		fucofulem1.5	|- ( ( ph /\ et ) -> ta )
6		simpl	|- ( ( ph /\ ps ) -> ph )
7	1	biimpa	|- ( ( ph /\ ps ) -> ( ch /\ th /\ ta ) )
8	7	simp2d	|- ( ( ph /\ ps ) -> th )
9	7	simp3d	|- ( ( ph /\ ps ) -> ta )
10	6 8 9 2	syl12anc	|- ( ( ph /\ ps ) -> et )
11		simpl	|- ( ( ph /\ et ) -> ph )
12	3	a1i	|- ( ( ph /\ et ) -> ch )
13	1	biimpar	|- ( ( ph /\ ( ch /\ th /\ ta ) ) -> ps )
14	11 12 4 5 13	syl13anc	|- ( ( ph /\ et ) -> ps )
15	10 14	impbida	|- ( ph -> ( ps <-> et ) )