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

Theorem necon1ai 3043
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 3041 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 135 1 (𝐴𝐵𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon1i  3049  opnz  5357  inisegn0  5955  iotan0  6339  tz6.12i  6690  fvfundmfvn0  6702  brfvopabrbr  6759  elfvmptrab1  6788  brovpreldm  7775  brovex  7879  brwitnlem  8123  cantnflem1  9141  carddomi2  9388  rankcf  10188  1re  10630  eliooxr  12785  iccssioo2  12799  elfzoel1  13026  elfzoel2  13027  ismnd  17904  lactghmga  18464  pmtrmvd  18515  mpfrcl  20228  fsubbas  22405  filuni  22423  ptcmplem2  22591  itg1climres  24244  mbfi1fseqlem4  24248  dvferm1lem  24510  dvferm2lem  24512  dvferm  24514  dvivthlem1  24534  coeeq2  24761  coe1termlem  24777  isppw  25619  dchrelbasd  25743  lgsne0  25839  wlkvv  27336  eldm3  32895  brfvimex  40256  brovmptimex  40257  clsneibex  40332  neicvgbex  40342  iotan0aiotaex  43172  afvnufveq  43227
  Copyright terms: Public domain W3C validator