Metamath Proof Explorer


Theorem sbceq1ddi

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 )

Proof

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 )