Theorem necon1ai 2688

Description: Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
necon1ai.1

Assertion

Ref	Expression
necon1ai

Proof of Theorem necon1ai

Step	Hyp	Ref	Expression
1		necon1ai.1	. . 3
2	1	necon3ai 2685	. 2
3	2	notnotrd 113	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652

This theorem is referenced by:  necon1i  2699  opnz  4723  tz6.12i  5891  elfvdm  5897  fvfundmfvn0  5903  elfvmptrab1  5976  bropopvvv  6880  brovex  6969  brwitnlem  7176  cantnflem1  8129  cantnflem1OLD  8152  carddomi2  8372  cdainf  8593  rankcf  9176  1re  9616  eliooxr  11612  iccssioo2  11626  elfzoel1  11827  elfzoel2  11828  ismnd  15923  ismndOLD  15926  lactghmga  16429  pmtrmvd  16481  mpfrcl  18187  fsubbas  20368  filuni  20386  ptcmplem2  20553  itg1climres  22121  mbfi1fseqlem4  22125  dvferm1lem  22385  dvferm2lem  22387  dvferm  22389  dvivthlem1  22409  coeeq2  22639  coe1termlem  22655  isppw  23388  dchrelbasd  23514  lgsne0  23608  clwwlknprop  24772  2wlkonot3v  24875  2spthonot3v  24876  eldm3  29191  inisegn0  30989  afvnufveq  32232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-ne 2654