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

Theorem necon2bi 2973
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
Hypothesis
Ref Expression
necon2bi.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
necon2bi (𝐴 = 𝐵 → ¬ 𝜑)

Proof of Theorem necon2bi
StepHypRef Expression
1 necon2bi.1 . . 3 (𝜑𝐴𝐵)
21neneqd 2948 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32con2i 136 1 (𝐴 = 𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1631  wne 2943
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 2944
This theorem is referenced by:  rzal  4214  difsnb  4472  dtrucor2  5029  kmlem6  9179  winainflem  9717  0npi  9906  0npr  10016  0nsr  10102  1div0  10888  rexmul  12306  rennim  14187  mrissmrcd  16508  prmirred  20058  pthaus  21662  rplogsumlem2  25395  pntrlog2bndlem4  25490  pntrlog2bndlem5  25491  1div0apr  27666  bnj1311  31430  subfacp1lem6  31505  bj-dtrucor2v  33137  itg2addnclem3  33795  cdleme31id  36203  sdrgacs  38297  rzalf  39698  jumpncnp  40629  fourierswlem  40964
  Copyright terms: Public domain W3C validator