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=23=3

Proof

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