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

Theorem necon1d 3043
Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon1d.1 (𝜑 → (𝐴𝐵𝐶 = 𝐷))
Assertion
Ref Expression
necon1d (𝜑 → (𝐶𝐷𝐴 = 𝐵))

Proof of Theorem necon1d
StepHypRef Expression
1 necon1d.1 . . 3 (𝜑 → (𝐴𝐵𝐶 = 𝐷))
2 nne 3025 . . 3 𝐶𝐷𝐶 = 𝐷)
31, 2syl6ibr 253 . 2 (𝜑 → (𝐴𝐵 → ¬ 𝐶𝐷))
43necon4ad 3040 1 (𝜑 → (𝐶𝐷𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wne 3021
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 3022
This theorem is referenced by:  disji  5046  mul02lem2  10811  xblss2ps  22945  xblss2  22946  lgsne0  25844  h1datomi  29291  eigorthi  29547  disjif  30262  lineintmo  33521  poimirlem6  34784  poimirlem7  34785  2llnmat  36546  2lnat  36806  tendospcanN  38045  dihmeetlem13N  38341  dochkrshp  38408  remul02  39119  remul01  39121
  Copyright terms: Public domain W3C validator