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

Theorem necon1ai 2958
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 2955 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 133 1 (𝐴𝐵𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1534  wne 2930
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 206  df-ne 2931
This theorem is referenced by:  necon1i  2964  opnz  5471  inisegn0  6100  iotan0  6536  tz6.12i  6921  fvfundmfvn0  6936  brfvopabrbr  6998  elfvmptrab1  7029  brovpreldm  8095  brovex  8229  brwitnlem  8529  cantnflem1  9725  carddomi2  10006  rankcf  10811  1re  11255  eliooxr  13430  iccssioo2  13445  elfzoel1  13678  elfzoel2  13679  ismnd  18725  lactghmga  19399  pmtrmvd  19450  mpfrcl  22096  mhpsclcl  22137  fsubbas  23859  filuni  23877  ptcmplem2  24045  itg1climres  25732  mbfi1fseqlem4  25736  dvferm1lem  26004  dvferm2lem  26006  dvferm  26008  dvivthlem1  26029  coeeq2  26266  coe1termlem  26282  isppw  27139  dchrelbasd  27265  lgsne0  27361  wlkvv  29561  eldm3  35596  brfvimex  43730  brovmptimex  43731  clsneibex  43806  neicvgbex  43816  iotan0aiotaex  46742  afvnufveq  46796  gricrcl  47498  grlicrcl  47533  grilcbri2  47537  fvconstr  48259  fvconstrn0  48260  fvconstr2  48261
  Copyright terms: Public domain W3C validator