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

Theorem necon1ai 2850
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 2848 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 128 1 (𝐴𝐵𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  necon1i  2856  opnz  4971  inisegn0  5532  tz6.12i  6252  elfvdm  6258  fvfundmfvn0  6264  brfvopabrbr  6318  elfvmptrab1  6344  brovpreldm  7299  brovex  7393  brwitnlem  7632  cantnflem1  8624  carddomi2  8834  cdainf  9052  rankcf  9637  1re  10077  eliooxr  12270  iccssioo2  12284  elfzoel1  12507  elfzoel2  12508  ismnd  17344  lactghmga  17870  pmtrmvd  17922  mpfrcl  19566  fsubbas  21718  filuni  21736  ptcmplem2  21904  itg1climres  23526  mbfi1fseqlem4  23530  dvferm1lem  23792  dvferm2lem  23794  dvferm  23796  dvivthlem1  23816  coeeq2  24043  coe1termlem  24059  isppw  24885  dchrelbasd  25009  lgsne0  25105  wlkvv  26578  eldm3  31777  brfvimex  38641  brovmptimex  38642  clsneibex  38717  neicvgbex  38727  afvnufveq  41548
  Copyright terms: Public domain W3C validator