Theorem necon3bd 2940

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon3bd.1	⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))

Assertion

Ref	Expression
necon3bd	⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Proof of Theorem necon3bd

Step	Hyp	Ref	Expression
1		nne 2930	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
2		necon3bd.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3	1, 2	biimtrid 242	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926

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 207  df-ne 2927

This theorem is referenced by:  necon2ad  2941  nssne1  4012  nssne2  4013  disjne  4421  nbrne1  5129  nbrne2  5130  peano5  7872  oeeui  8569  domdifsn  9028  ac6sfi  9238  inf3lem2  9589  cnfcom3lem  9663  dfac9  10097  fin23lem21  10299  1re  11181  dedekindle  11345  zneo  12624  modirr  13914  sqrmo  15224  reusq0  15438  pc2dvds  16857  pcadd  16867  oddprmdvds  16881  4sqlem11  16933  latnlej  18422  sylow2blem3  19559  irredn0  20339  irredn1  20342  isnzr2  20434  lssvneln0  20865  lspsnne2  21035  lspfixed  21045  lspindpi  21049  lsmcv  21058  lspsolv  21060  coe1tmmul  22170  dfac14  23512  fbdmn0  23728  filufint  23814  flimfnfcls  23922  alexsubALTlem2  23942  evth  24865  cphsqrtcl2  25093  ovolicc2lem4  25428  lhop1lem  25925  lhop1  25926  lhop2  25927  lhop  25928  deg1add  26015  abelthlem2  26349  logcnlem2  26559  angpined  26747  asinneg  26803  dmgmaddn0  26940  lgsne0  27253  lgsqr  27269  lgsquadlem2  27299  lgsquadlem3  27300  axlowdimlem17  28892  spansncvi  31588  argcj  32679  constrrecl  33766  zarcmplem  33878  broutsideof2  36117  unblimceq0lem  36501  poimirlem28  37649  dvasin  37705  dvacos  37706  nninfnub  37752  dvrunz  37955  lsatcvatlem  39049  lkrlsp2  39103  opnlen0  39188  2llnne2N  39409  lnnat  39428  llnn0  39517  lplnn0N  39548  lplnllnneN  39557  llncvrlpln2  39558  llncvrlpln  39559  lvoln0N  39592  lplncvrlvol2  39616  lplncvrlvol  39617  dalempnes  39652  dalemqnet  39653  dalemcea  39661  dalem3  39665  cdlema1N  39792  cdlemb  39795  paddasslem5  39825  llnexchb2lem  39869  osumcllem4N  39960  pexmidlem1N  39971  lhp2lt  40002  lhp2atne  40035  lhp2at0ne  40037  4atexlemunv  40067  4atexlemex2  40072  trlne  40186  trlval4  40189  cdlemc4  40195  cdleme11dN  40263  cdleme11h  40267  cdlemednuN  40301  cdleme20j  40319  cdleme20k  40320  cdleme21at  40329  cdleme35f  40455  cdlemg11b  40643  dia2dimlem1  41065  dihmeetlem3N  41306  dihmeetlem15N  41322  dochsnnz  41451  dochexmidlem1  41461  dochexmidlem7  41467  mapdindp3  41723  fltne  42639  pellexlem1  42824  dfac21  43062  pm13.14  44405  uzlidlring  48227  suppdm  48503