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 )