Metamath Proof Explorer
Description: Contrapositive inference for inequality. (Contributed by NM, 12Feb2007) (Proof shortened by Wolf Lammen, 22Nov2019)


Ref 
Expression 

Hypothesis 
necon1ai.1 
$${\u22a2}\neg {\phi}\to {A}={B}$$ 

Assertion 
necon1ai 
$${\u22a2}{A}\ne {B}\to {\phi}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

necon1ai.1 
$${\u22a2}\neg {\phi}\to {A}={B}$$ 
2 
1

necon3ai 
$${\u22a2}{A}\ne {B}\to \neg \neg {\phi}$$ 
3 
2

notnotrd 
$${\u22a2}{A}\ne {B}\to {\phi}$$ 