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

Theorem necon1ai 2809
 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 2807 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 127 1 (𝐴𝐵𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  necon1i  2815  opnz  4868  inisegn0  5416  tz6.12i  6124  elfvdm  6130  fvfundmfvn0  6136  elfvmptrab1  6213  brovpreldm  7141  brovex  7235  brwitnlem  7474  cantnflem1  8469  carddomi2  8679  cdainf  8897  rankcf  9478  1re  9918  eliooxr  12103  iccssioo2  12117  elfzoel1  12337  elfzoel2  12338  ismnd  17120  lactghmga  17647  pmtrmvd  17699  mpfrcl  19339  fsubbas  21481  filuni  21499  ptcmplem2  21667  itg1climres  23287  mbfi1fseqlem4  23291  dvferm1lem  23551  dvferm2lem  23553  dvferm  23555  dvivthlem1  23575  coeeq2  23802  coe1termlem  23818  isppw  24640  dchrelbasd  24764  lgsne0  24860  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  eldm3  30905  brfvimex  37344  brovmptimex  37345  clsneibex  37420  neicvgbex  37430  afvnufveq  39876  1wlkvv  40831
 Copyright terms: Public domain W3C validator