Metamath Proof Explorer


Theorem ex-an

Description: Example for df-an . Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion ex-an 2 = 2 3 = 3

Proof

Step Hyp Ref Expression
1 eqid 2 = 2
2 eqid 3 = 3
3 1 2 pm3.2i 2 = 2 3 = 3