This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem z2even

Description: 2 divides 2. That means 2 is even. (Contributed by AV, 12-Feb-2020) (Revised by AV, 23-Jun-2021)

Ref Expression
Assertion z2even 2 ∥ 2

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 iddvds ⊢ ( 2 ∈ ℤ → 2 ∥ 2 )
3 1 2 ax-mp ⊢ 2 ∥ 2