Theorem functermclem

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

	Ref	Expression
Hypotheses	functermclem.1	|- ( ( ph /\ K R L ) -> K = F )
	functermclem.2	|- ( ph -> ( F R L <-> L = G ) )
Assertion	functermclem	|- ( ph -> ( K R L <-> ( K = F /\ L = G ) ) )

Proof

Step	Hyp	Ref	Expression
1		functermclem.1	|- ( ( ph /\ K R L ) -> K = F )
2		functermclem.2	|- ( ph -> ( F R L <-> L = G ) )
3		simpr	|- ( ( ph /\ K R L ) -> K R L )
4	1 3	eqbrtrrd	|- ( ( ph /\ K R L ) -> F R L )
5	2	biimpa	|- ( ( ph /\ F R L ) -> L = G )
6	4 5	syldan	|- ( ( ph /\ K R L ) -> L = G )
7	1 6	jca	|- ( ( ph /\ K R L ) -> ( K = F /\ L = G ) )
8		simprl	|- ( ( ph /\ ( K = F /\ L = G ) ) -> K = F )
9	2	biimpar	|- ( ( ph /\ L = G ) -> F R L )
10	9	adantrl	|- ( ( ph /\ ( K = F /\ L = G ) ) -> F R L )
11	8 10	eqbrtrd	|- ( ( ph /\ ( K = F /\ L = G ) ) -> K R L )
12	7 11	impbida	|- ( ph -> ( K R L <-> ( K = F /\ L = G ) ) )