Theorem sbceq1ddi

Description: A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019)

	Ref	Expression
Hypotheses	sbceq1ddi.1	$$⊢\phi \to A=B$$
	sbceq1ddi.2	$$⊢\psi \to \theta$$
	sbceq1ddi.3	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \leftrightarrow \theta$$
	sbceq1ddi.4	$$⊢\underset{\dot{}}{[}B/x\underset{\dot{}}{]}\chi \leftrightarrow \eta$$
Assertion	sbceq1ddi	$$⊢\left(\phi \wedge \psi \right)\to \eta$$

Proof

Step	Hyp	Ref	Expression
1		sbceq1ddi.1	$$⊢\phi \to A=B$$
2		sbceq1ddi.2	$$⊢\psi \to \theta$$
3		sbceq1ddi.3	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \leftrightarrow \theta$$
4		sbceq1ddi.4	$$⊢\underset{\dot{}}{[}B/x\underset{\dot{}}{]}\chi \leftrightarrow \eta$$
5	1	adantr	$$⊢\left(\phi \wedge \psi \right)\to A=B$$
6	2 3	sylibr	$$⊢\psi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi$$
7	6	adantl	$$⊢\left(\phi \wedge \psi \right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi$$
8	5 7	sbceq1dd	$$⊢\left(\phi \wedge \psi \right)\to \underset{\dot{}}{[}B/x\underset{\dot{}}{]}\chi$$
9	8 4	sylib	$$⊢\left(\phi \wedge \psi \right)\to \eta$$