Metamath Proof Explorer


Theorem ex-pr

Description: Example for df-pr . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-pr A 1 1 A 2 = 1

Proof

Step Hyp Ref Expression
1 elpri A 1 1 A = 1 A = 1
2 oveq1 A = 1 A 2 = 1 2
3 sq1 1 2 = 1
4 2 3 eqtrdi A = 1 A 2 = 1
5 oveq1 A = 1 A 2 = 1 2
6 neg1sqe1 1 2 = 1
7 5 6 eqtrdi A = 1 A 2 = 1
8 4 7 jaoi A = 1 A = 1 A 2 = 1
9 1 8 syl A 1 1 A 2 = 1