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

Theorem necon1ai 2959
 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 2957 . 2 (𝐴𝐵 → ¬ ¬ 𝜑)
32notnotrd 128 1 (𝐴𝐵𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1632   ≠ wne 2932 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 197  df-ne 2933 This theorem is referenced by:  necon1i  2965  opnz  5090  inisegn0  5655  tz6.12i  6375  elfvdm  6381  fvfundmfvn0  6387  brfvopabrbr  6441  elfvmptrab1  6467  brovpreldm  7422  brovex  7517  brwitnlem  7756  cantnflem1  8759  carddomi2  8986  cdainf  9206  rankcf  9791  1re  10231  eliooxr  12425  iccssioo2  12439  elfzoel1  12662  elfzoel2  12663  ismnd  17498  lactghmga  18024  pmtrmvd  18076  mpfrcl  19720  fsubbas  21872  filuni  21890  ptcmplem2  22058  itg1climres  23680  mbfi1fseqlem4  23684  dvferm1lem  23946  dvferm2lem  23948  dvferm  23950  dvivthlem1  23970  coeeq2  24197  coe1termlem  24213  isppw  25039  dchrelbasd  25163  lgsne0  25259  wlkvv  26732  eldm3  31958  brfvimex  38826  brovmptimex  38827  clsneibex  38902  neicvgbex  38912  afvnufveq  41733
 Copyright terms: Public domain W3C validator