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

Theorem necon1ai 2808
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 2806 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 126 1 (𝐴𝐵𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2779
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 195  df-ne 2781
This theorem is referenced by:  necon1i  2814  opnz  4861  inisegn0  5402  tz6.12i  6108  elfvdm  6114  fvfundmfvn0  6120  elfvmptrab1  6197  brovpreldm  7118  brovex  7212  brwitnlem  7451  cantnflem1  8446  carddomi2  8656  cdainf  8874  rankcf  9455  1re  9895  eliooxr  12061  iccssioo2  12075  elfzoel1  12294  elfzoel2  12295  ismnd  17068  lactghmga  17595  pmtrmvd  17647  mpfrcl  19287  fsubbas  21428  filuni  21446  ptcmplem2  21614  itg1climres  23231  mbfi1fseqlem4  23235  dvferm1lem  23495  dvferm2lem  23497  dvferm  23499  dvivthlem1  23519  coeeq2  23746  coe1termlem  23762  isppw  24584  dchrelbasd  24708  lgsne0  24804  clwwlknprop  26093  2wlkonot3v  26195  2spthonot3v  26196  eldm3  30698  brfvimex  37127  brovmptimex  37128  clsneibex  37203  neicvgbex  37213  afvnufveq  39660  1wlkvv  40812
  Copyright terms: Public domain W3C validator