| 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 ) ) ) |