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

Theorem necon1ai 3017
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 3015 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 135 1 (𝐴𝐵𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wne 2990
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 210  df-ne 2991
This theorem is referenced by:  necon1i  3023  opnz  5333  inisegn0  5932  iotan0  6318  tz6.12i  6675  fvfundmfvn0  6687  brfvopabrbr  6746  elfvmptrab1  6776  brovpreldm  7771  brovex  7875  brwitnlem  8119  cantnflem1  9140  carddomi2  9387  rankcf  10192  1re  10634  eliooxr  12787  iccssioo2  12802  elfzoel1  13035  elfzoel2  13036  ismnd  17909  lactghmga  18528  pmtrmvd  18579  mpfrcl  20760  fsubbas  22475  filuni  22493  ptcmplem2  22661  itg1climres  24321  mbfi1fseqlem4  24325  dvferm1lem  24590  dvferm2lem  24592  dvferm  24594  dvivthlem1  24614  coeeq2  24842  coe1termlem  24858  isppw  25702  dchrelbasd  25826  lgsne0  25922  wlkvv  27419  eldm3  33105  brfvimex  40716  brovmptimex  40717  clsneibex  40792  neicvgbex  40802  iotan0aiotaex  43635  afvnufveq  43690
  Copyright terms: Public domain W3C validator