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

Theorem necon1bi 3047
Description: Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
necon1bi.1 (𝐴𝐵𝜑)
Assertion
Ref Expression
necon1bi 𝜑𝐴 = 𝐵)

Proof of Theorem necon1bi
StepHypRef Expression
1 df-ne 3020 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bi.1 . . 3 (𝐴𝐵𝜑)
31, 2sylbir 237 . 2 𝐴 = 𝐵𝜑)
43con1i 149 1 𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1536  wne 3019
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 209  df-ne 3020
This theorem is referenced by:  necon4ai  3050  fvbr0  6700  peano5  7608  1stnpr  7696  2ndnpr  7697  1st2val  7720  2nd2val  7721  eceqoveq  8405  mapprc  8413  ixp0  8498  setind  9179  hashfun  13801  hashf1lem2  13817  iswrdi  13868  ffz0iswrd  13894  dvdsrval  19398  thlle  20844  konigsberg  28039  hatomistici  30142  esumrnmpt2  31331  mppsval  32823  setindtr  39627  fourierdlem72  42470  afvpcfv0  43352
  Copyright terms: Public domain W3C validator