Description: A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sbceq1ddi.1 | |- ( ph -> A = B ) |
|
sbceq1ddi.2 | |- ( ps -> th ) |
||
sbceq1ddi.3 | |- ( [. A / x ]. ch <-> th ) |
||
sbceq1ddi.4 | |- ( [. B / x ]. ch <-> et ) |
||
Assertion | sbceq1ddi | |- ( ( ph /\ ps ) -> et ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbceq1ddi.1 | |- ( ph -> A = B ) |
|
2 | sbceq1ddi.2 | |- ( ps -> th ) |
|
3 | sbceq1ddi.3 | |- ( [. A / x ]. ch <-> th ) |
|
4 | sbceq1ddi.4 | |- ( [. B / x ]. ch <-> et ) |
|
5 | 1 | adantr | |- ( ( ph /\ ps ) -> A = B ) |
6 | 2 3 | sylibr | |- ( ps -> [. A / x ]. ch ) |
7 | 6 | adantl | |- ( ( ph /\ ps ) -> [. A / x ]. ch ) |
8 | 5 7 | sbceq1dd | |- ( ( ph /\ ps ) -> [. B / x ]. ch ) |
9 | 8 4 | sylib | |- ( ( ph /\ ps ) -> et ) |