Theorem sbceq1ddi

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

	Ref	Expression
Hypotheses	sbceq1ddi.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	sbceq1ddi.2	⊢ ( 𝜓 → 𝜃 )
	sbceq1ddi.3	⊢ ( [ 𝐴 / 𝑥 ] 𝜒 ↔ 𝜃 )
	sbceq1ddi.4	⊢ ( [ 𝐵 / 𝑥 ] 𝜒 ↔ 𝜂 )
Assertion	sbceq1ddi	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		sbceq1ddi.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		sbceq1ddi.2	⊢ ( 𝜓 → 𝜃 )
3		sbceq1ddi.3	⊢ ( [ 𝐴 / 𝑥 ] 𝜒 ↔ 𝜃 )
4		sbceq1ddi.4	⊢ ( [ 𝐵 / 𝑥 ] 𝜒 ↔ 𝜂 )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 )
6	2 3	sylibr	⊢ ( 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → [ 𝐴 / 𝑥 ] 𝜒 )
8	5 7	sbceq1dd	⊢ ( ( 𝜑 ∧ 𝜓 ) → [ 𝐵 / 𝑥 ] 𝜒 )
9	8 4	sylib	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜂 )