Theorem necon3bd 2974

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  necon2ad  2975  nssne1  4001  nssne2  4002  disjne  4412  nbrne1  5124  nbrne2  5125  peano5  7878  oeeui  8576  domdifsn  9036  ac6sfi  9232  inf3lem2  9586  cnfcom3lem  9660  dfac9  10108  fin23lem21  10311  1re  11196  dedekindle  11362  zneo  12670  modirr  13969  sqrmo  15292  reusq0  15506  pc2dvds  16929  pcadd  16939  oddprmdvds  16953  4sqlem11  17005  latnlej  18502  sylow2blem3  19683  irredn0  20496  irredn1  20499  isnzr2  20592  lssvneln0  21042  lspsnne2  21211  lspfixed  21221  lspindpi  21225  lsmcv  21234  lspsolv  21236  coe1tmmul  22398  dfac14  23736  fbdmn0  23952  filufint  24038  flimfnfcls  24146  alexsubALTlem2  24166  evth  25079  cphsqrtcl2  25306  ovolicc2lem4  25640  lhop1lem  26133  lhop1  26134  lhop2  26135  lhop  26136  deg1add  26221  abelthlem2  26553  logcnlem2  26766  angpined  26953  asinneg  27009  dmgmaddn0  27145  lgsne0  27457  lgsqr  27473  lgsquadlem2  27503  lgsquadlem3  27504  axlowdimlem17  29217  spansncvi  31913  argcj  33005  constrrecl  34076  zarcmplem  34188  broutsideof2  36485  unblimceq0lem  36957  poimirlem28  38159  dvasin  38215  dvacos  38216  nninfnub  38262  dvrunz  38465  lsatcvatlem  39685  lkrlsp2  39739  opnlen0  39824  2llnne2N  40044  lnnat  40063  llnn0  40152  lplnn0N  40183  lplnllnneN  40192  llncvrlpln2  40193  llncvrlpln  40194  lvoln0N  40227  lplncvrlvol2  40251  lplncvrlvol  40252  dalempnes  40287  dalemqnet  40288  dalemcea  40296  dalem3  40300  cdlema1N  40427  cdlemb  40430  paddasslem5  40460  llnexchb2lem  40504  osumcllem4N  40595  pexmidlem1N  40606  lhp2lt  40637  lhp2atne  40670  lhp2at0ne  40672  4atexlemunv  40702  4atexlemex2  40707  trlne  40821  trlval4  40824  cdlemc4  40830  cdleme11dN  40898  cdleme11h  40902  cdlemednuN  40936  cdleme20j  40954  cdleme20k  40955  cdleme21at  40964  cdleme35f  41090  cdlemg11b  41278  dia2dimlem1  41700  dihmeetlem3N  41941  dihmeetlem15N  41957  dochsnnz  42086  dochexmidlem1  42096  dochexmidlem7  42102  mapdindp3  42358  fltne  43238  pellexlem1  43418  dfac21  43655  pm13.14  44983  uzlidlring  48855  suppdm  49141