Metamath Proof Explorer


Theorem pr2nelemOLD

Description: Obsolete version of enpr2 as of 30-Dec-2024. (Contributed by FL, 17-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pr2nelemOLD A C B D A B A B 2 𝑜

Proof

Step Hyp Ref Expression
1 disjsn2 A B A B =
2 ensn1g A C A 1 𝑜
3 ensn1g B D B 1 𝑜
4 pm54.43 A 1 𝑜 B 1 𝑜 A B = A B 2 𝑜
5 df-pr A B = A B
6 5 breq1i A B 2 𝑜 A B 2 𝑜
7 4 6 bitr4di A 1 𝑜 B 1 𝑜 A B = A B 2 𝑜
8 7 biimpd A 1 𝑜 B 1 𝑜 A B = A B 2 𝑜
9 2 3 8 syl2an A C B D A B = A B 2 𝑜
10 9 ex A C B D A B = A B 2 𝑜
11 1 10 syl7 A C B D A B A B 2 𝑜
12 11 3imp A C B D A B A B 2 𝑜