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

Metamath Proof Explorer

Theorem neeq12i

Description: Inference for inequality. (Contributed by NM, 24-Jul-2012) (Proof shortened by Wolf Lammen, 25-Nov-2019)

Ref Expression
Hypotheses neeq1i.1 ⊢ 𝐴 = 𝐵
neeq12i.2 ⊢ 𝐶 = 𝐷
Assertion neeq12i ( 𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷 )

Proof

Step Hyp Ref Expression
1 neeq1i.1 ⊢ 𝐴 = 𝐵
2 neeq12i.2 ⊢ 𝐶 = 𝐷
3 1 2 eqeq12i ⊢ ( 𝐴 = 𝐶 ↔ 𝐵 = 𝐷 )
4 3 necon3bii ⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷 )