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

Theorem necon1ai 2991
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 2989 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 131 1 (𝐴𝐵𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1507  wne 2964
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 199  df-ne 2965
This theorem is referenced by:  necon1i  2997  opnz  5219  inisegn0  5799  tz6.12i  6523  elfvdmOLD  6530  fvfundmfvn0  6536  brfvopabrbr  6590  elfvmptrab1  6618  brovpreldm  7589  brovex  7688  brwitnlem  7930  cantnflem1  8942  carddomi2  9189  rankcf  9993  1re  10435  eliooxr  12608  iccssioo2  12622  elfzoel1  12849  elfzoel2  12850  ismnd  17759  lactghmga  18287  pmtrmvd  18339  mpfrcl  20005  fsubbas  22173  filuni  22191  ptcmplem2  22359  itg1climres  24012  mbfi1fseqlem4  24016  dvferm1lem  24278  dvferm2lem  24280  dvferm  24282  dvivthlem1  24302  coeeq2  24529  coe1termlem  24545  isppw  25387  dchrelbasd  25511  lgsne0  25607  wlkvv  27105  eldm3  32487  brfvimex  39717  brovmptimex  39718  clsneibex  39793  neicvgbex  39803  iotan0aiotaex  42676  afvnufveq  42731
  Copyright terms: Public domain W3C validator