fucofulem1

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

	Ref	Expression
Hypotheses	fucofulem1.1	$⊢ φ \to (ψ \leftrightarrow (χ \land θ \land τ))$
	fucofulem1.2	$⊢ (φ \land (θ \land τ)) \to η$
	fucofulem1.3	$⊢ χ$
	fucofulem1.4	$⊢ (φ \land η) \to θ$
	fucofulem1.5	$⊢ (φ \land η) \to τ$
Assertion	fucofulem1	$⊢ φ \to (ψ \leftrightarrow η)$

Step	Hyp	Ref	Expression
1		fucofulem1.1	$⊢ φ \to (ψ \leftrightarrow (χ \land θ \land τ))$
2		fucofulem1.2	$⊢ (φ \land (θ \land τ)) \to η$
3		fucofulem1.3	$⊢ χ$
4		fucofulem1.4	$⊢ (φ \land η) \to θ$
5		fucofulem1.5	$⊢ (φ \land η) \to τ$
6		simpl	$⊢ (φ \land ψ) \to φ$
7	1	biimpa	$⊢ (φ \land ψ) \to (χ \land θ \land τ)$
8	7	simp2d	$⊢ (φ \land ψ) \to θ$
9	7	simp3d	$⊢ (φ \land ψ) \to τ$
10	6 8 9 2	syl12anc	$⊢ (φ \land ψ) \to η$
11		simpl	$⊢ (φ \land η) \to φ$
12	3	a1i	$⊢ (φ \land η) \to χ$
13	1	biimpar	$⊢ (φ \land (χ \land θ \land τ)) \to ψ$
14	11 12 4 5 13	syl13anc	$⊢ (φ \land η) \to ψ$
15	10 14	impbida	$⊢ φ \to (ψ \leftrightarrow η)$

Metamath Proof Explorer