Metamath Proof Explorer


Theorem altopeq12

Description: Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012)

Ref Expression
Assertion altopeq12 A=BC=DAC=BD

Proof

Step Hyp Ref Expression
1 sneq A=BA=B
2 sneq C=DC=D
3 1 2 anim12i A=BC=DA=BC=D
4 altopthsn AC=BDA=BC=D
5 3 4 sylibr A=BC=DAC=BD