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 )