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

Theorem necon1ai 2967
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 2964 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 133 1 (𝐴𝐵𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2939
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 207  df-ne 2940
This theorem is referenced by:  necon1i  2973  opnz  5477  inisegn0  6115  iotan0  6550  tz6.12i  6933  fvfundmfvn0  6948  brfvopabrbr  7012  elfvmptrab1  7043  brovpreldm  8115  brovex  8248  brwitnlem  8546  cantnflem1  9730  carddomi2  10011  rankcf  10818  1re  11262  eliooxr  13446  iccssioo2  13461  elfzoel1  13698  elfzoel2  13699  ismnd  18751  lactghmga  19424  pmtrmvd  19475  mpfrcl  22110  mhpsclcl  22152  fsubbas  23876  filuni  23894  ptcmplem2  24062  itg1climres  25750  mbfi1fseqlem4  25754  dvferm1lem  26023  dvferm2lem  26025  dvferm  26027  dvivthlem1  26048  coeeq2  26282  coe1termlem  26298  isppw  27158  dchrelbasd  27284  lgsne0  27380  wlkvv  29646  eldm3  35762  brfvimex  44044  brovmptimex  44045  clsneibex  44120  neicvgbex  44130  iotan0aiotaex  47110  afvnufveq  47164  gricrcl  47888  grlicrcl  47972  grilcbri2  47976  fvconstr  48770  fvconstrn0  48771  fvconstr2  48772
  Copyright terms: Public domain W3C validator