Metamath Proof Explorer


Theorem elequ12

Description: An identity law for the non-logical predicate, which combines elequ1 and elequ2 . The analogous theorems for class terms are eleq1 , eleq2 , and eleq12 respectively. (Contributed by BJ, 29-Sep-2019)

Ref Expression
Assertion elequ12 ( ( 𝑥 = 𝑦𝑧 = 𝑡 ) → ( 𝑥𝑧𝑦𝑡 ) )

Proof

Step Hyp Ref Expression
1 elequ1 ( 𝑥 = 𝑦 → ( 𝑥𝑧𝑦𝑧 ) )
2 elequ2 ( 𝑧 = 𝑡 → ( 𝑦𝑧𝑦𝑡 ) )
3 1 2 sylan9bb ( ( 𝑥 = 𝑦𝑧 = 𝑡 ) → ( 𝑥𝑧𝑦𝑡 ) )