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

Step	Hyp	Ref	Expression
1		notnot 142	. 2 ⊢ (𝜓 → ¬ ¬ 𝜓)
2		necon4ad.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))
3	2	necon1bd 2947	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵))
4	1, 3	syl5 34	1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))

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