Theorem necon3bd 2949

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 2939	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
2		necon3bd.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3	1, 2	biimtrid 243	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 2936

This theorem is referenced by:  necon2ad  2950  nssne1  3984  nssne2  3985  disjne  4390  nbrne1  5098  nbrne2  5099  peano5  7840  oeeui  8535  domdifsn  8995  ac6sfi  9191  inf3lem2  9548  cnfcom3lem  9622  dfac9  10057  fin23lem21  10259  1re  11142  dedekindle  11308  zneo  12610  modirr  13902  sqrmo  15211  reusq0  15425  pc2dvds  16848  pcadd  16858  oddprmdvds  16872  4sqlem11  16924  latnlej  18420  sylow2blem3  19595  irredn0  20401  irredn1  20404  isnzr2  20497  lssvneln0  20949  lspsnne2  21118  lspfixed  21128  lspindpi  21132  lsmcv  21141  lspsolv  21143  coe1tmmul  22270  dfac14  23608  fbdmn0  23824  filufint  23910  flimfnfcls  24018  alexsubALTlem2  24038  evth  24951  cphsqrtcl2  25178  ovolicc2lem4  25512  lhop1lem  26005  lhop1  26006  lhop2  26007  lhop  26008  deg1add  26093  abelthlem2  26422  logcnlem2  26632  angpined  26819  asinneg  26875  dmgmaddn0  27011  lgsne0  27323  lgsqr  27339  lgsquadlem2  27369  lgsquadlem3  27370  axlowdimlem17  29052  spansncvi  31748  argcj  32847  constrrecl  33960  zarcmplem  34072  broutsideof2  36357  unblimceq0lem  36819  poimirlem28  38022  dvasin  38078  dvacos  38079  nninfnub  38125  dvrunz  38328  lsatcvatlem  39548  lkrlsp2  39602  opnlen0  39687  2llnne2N  39907  lnnat  39926  llnn0  40015  lplnn0N  40046  lplnllnneN  40055  llncvrlpln2  40056  llncvrlpln  40057  lvoln0N  40090  lplncvrlvol2  40114  lplncvrlvol  40115  dalempnes  40150  dalemqnet  40151  dalemcea  40159  dalem3  40163  cdlema1N  40290  cdlemb  40293  paddasslem5  40323  llnexchb2lem  40367  osumcllem4N  40458  pexmidlem1N  40469  lhp2lt  40500  lhp2atne  40533  lhp2at0ne  40535  4atexlemunv  40565  4atexlemex2  40570  trlne  40684  trlval4  40687  cdlemc4  40693  cdleme11dN  40761  cdleme11h  40765  cdlemednuN  40799  cdleme20j  40817  cdleme20k  40818  cdleme21at  40827  cdleme35f  40953  cdlemg11b  41141  dia2dimlem1  41563  dihmeetlem3N  41804  dihmeetlem15N  41820  dochsnnz  41949  dochexmidlem1  41959  dochexmidlem7  41965  mapdindp3  42221  fltne  43101  pellexlem1  43281  dfac21  43518  pm13.14  44860  uzlidlring  48733  suppdm  49008