functermclem

	Ref	Expression
Hypotheses	functermclem.1	$⊢ (φ \land K R L) \to K = F$
	functermclem.2	$⊢ φ \to (F R L \leftrightarrow L = G)$
Assertion	functermclem	$⊢ φ \to (K R L \leftrightarrow (K = F \land L = G))$

Step	Hyp	Ref	Expression
1		functermclem.1	$⊢ (φ \land K R L) \to K = F$
2		functermclem.2	$⊢ φ \to (F R L \leftrightarrow L = G)$
3		simpr	$⊢ (φ \land K R L) \to K R L$
4	1 3	eqbrtrrd	$⊢ (φ \land K R L) \to F R L$
5	2	biimpa	$⊢ (φ \land F R L) \to L = G$
6	4 5	syldan	$⊢ (φ \land K R L) \to L = G$
7	1 6	jca	$⊢ (φ \land K R L) \to (K = F \land L = G)$
8		simprl	$⊢ (φ \land (K = F \land L = G)) \to K = F$
9	2	biimpar	$⊢ (φ \land L = G) \to F R L$
10	9	adantrl	$⊢ (φ \land (K = F \land L = G)) \to F R L$
11	8 10	eqbrtrd	$⊢ (φ \land (K = F \land L = G)) \to K R L$
12	7 11	impbida	$⊢ φ \to (K R L \leftrightarrow (K = F \land L = G))$

Metamath Proof Explorer