Metamath Proof Explorer


Theorem bj-elequ12

Description: An identity law for the non-logical predicate, which combines elequ1 and elequ2 . For the analogous theorems for class terms, see eleq1 , eleq2 and eleq12 . TODO: move to main part. (Contributed by BJ, 29-Sep-2019)

Ref Expression
Assertion bj-elequ12 x = y z = t x z y t

Proof

Step Hyp Ref Expression
1 elequ1 x = y x z y z
2 elequ2 z = t y z y t
3 1 2 sylan9bb x = y z = t x z y t