Metamath Proof Explorer


Theorem preq12i

Description: Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012)

Ref Expression
Hypotheses preq1i.1 A=B
preq12i.2 C=D
Assertion preq12i AC=BD

Proof

Step Hyp Ref Expression
1 preq1i.1 A=B
2 preq12i.2 C=D
3 preq12 A=BC=DAC=BD
4 1 2 3 mp2an AC=BD