MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon1ai Unicode version

Theorem necon1ai 2684
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
StepHypRef Expression
1 necon1ai.1 . . 3
21necon3ai 2681 . 2
32notnotrd 113 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1370  =/=wne 2648
This theorem is referenced by:  necon1i  2695  opnz  4680  tz6.12i  5833  elfvdm  5839  fvfundmfvn0  5845  bropopvvv  6786  brovex  6874  brwitnlem  7081  cantnflem1  8034  cantnflem1OLD  8057  carddomi2  8277  cdainf  8498  rankcf  9081  1re  9522  eliooxr  11493  iccssioo2  11507  elfzoel1  11696  elfzoel2  11697  ismnd  15576  lactghmga  16068  pmtrmvd  16121  mpfrcl  17781  fsubbas  19839  filuni  19857  ptcmplem2  20024  itg1climres  21592  mbfi1fseqlem4  21596  dvferm1lem  21856  dvferm2lem  21858  dvferm  21860  dvivthlem1  21880  coeeq2  22110  coe1termlem  22125  isppw  22852  dchrelbasd  22978  lgsne0  23072  eldm3  28028  inisegn0  29856  afvnufveq  30930  elfvmptrab1  31031  2wlkonot3v  31271  2spthonot3v  31272  clwwlknprop  31312
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 2650
  Copyright terms: Public domain W3C validator