Metamath Proof Explorer


Theorem en2snOLDOLD

Description: Obsolete version of en2sn as of 31-Jul-2024. (Contributed by NM, 9-Nov-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en2snOLDOLD A C B D A B

Proof

Step Hyp Ref Expression
1 ensn1g A C A 1 𝑜
2 ensn1g B D B 1 𝑜
3 2 ensymd B D 1 𝑜 B
4 entr A 1 𝑜 1 𝑜 B A B
5 1 3 4 syl2an A C B D A B