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

Theorem necon4ad 2948
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon4ad.1 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
Assertion
Ref Expression
necon4ad (𝜑 → (𝜓𝐴 = 𝐵))

Proof of Theorem necon4ad
StepHypRef Expression
1 notnot 142 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon4ad.1 . . 3 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
32necon1bd 2947 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1533  wne 2929
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 206  df-ne 2930
This theorem is referenced by:  necon1d  2951  fisseneq  9282  f1finf1o  9296  f1finf1oOLD  9297  dfac5  10153  isf32lem9  10386  fpwwe2  10668  qextlt  13217  qextle  13218  xsubge0  13275  hashf1  14454  climuni  15532  rpnnen2lem12  16205  fzo0dvdseq  16303  4sqlem11  16927  haust1  23300  deg1lt0  26071  ply1divmo  26116  ig1peu  26154  dgrlt  26246  quotcan  26289  fta  27057  atcv0eq  32261  erdszelem9  34937  poimirlem23  37244  poimir  37254  lshpdisj  38586  lsatcv0eq  38646  exatleN  39004  atcvr0eq  39026  cdlemg31c  40299  itrere  42011  sn-itrere  42153  sn-retire  42154  jm2.19  42553  jm2.26lem3  42561  dgraa0p  42712
  Copyright terms: Public domain W3C validator