Theorem necon3bd 2978

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 2965

This theorem is referenced by:  necon2ad  2979  nssne1  4007  nssne2  4008  disjne  4421  nbrne1  5134  nbrne2  5135  peano5  7889  oeeui  8587  domdifsn  9047  ac6sfi  9243  inf3lem2  9597  cnfcom3lem  9671  dfac9  10119  fin23lem21  10322  1re  11207  dedekindle  11373  zneo  12678  modirr  13977  sqrmo  15301  reusq0  15515  pc2dvds  16938  pcadd  16948  oddprmdvds  16962  4sqlem11  17014  latnlej  18511  sylow2blem3  19691  irredn0  20504  irredn1  20507  isnzr2  20600  lssvneln0  21050  lspsnne2  21219  lspfixed  21229  lspindpi  21233  lsmcv  21242  lspsolv  21244  coe1tmmul  22406  dfac14  23743  fbdmn0  23959  filufint  24045  flimfnfcls  24153  alexsubALTlem2  24173  evth  25086  cphsqrtcl2  25313  ovolicc2lem4  25647  lhop1lem  26140  lhop1  26141  lhop2  26142  lhop  26143  deg1add  26228  abelthlem2  26560  logcnlem2  26773  angpined  26960  asinneg  27016  dmgmaddn0  27152  lgsne0  27464  lgsqr  27480  lgsquadlem2  27510  lgsquadlem3  27511  axlowdimlem17  29248  spansncvi  31944  argcj  33033  constrrecl  34103  zarcmplem  34215  broutsideof2  36512  unblimceq0lem  36983  poimirlem28  38186  dvasin  38242  dvacos  38243  nninfnub  38289  dvrunz  38492  lsatcvatlem  39712  lkrlsp2  39766  opnlen0  39851  2llnne2N  40071  lnnat  40090  llnn0  40179  lplnn0N  40210  lplnllnneN  40219  llncvrlpln2  40220  llncvrlpln  40221  lvoln0N  40254  lplncvrlvol2  40278  lplncvrlvol  40279  dalempnes  40314  dalemqnet  40315  dalemcea  40323  dalem3  40327  cdlema1N  40454  cdlemb  40457  paddasslem5  40487  llnexchb2lem  40531  osumcllem4N  40622  pexmidlem1N  40633  lhp2lt  40664  lhp2atne  40697  lhp2at0ne  40699  4atexlemunv  40729  4atexlemex2  40734  trlne  40848  trlval4  40851  cdlemc4  40857  cdleme11dN  40925  cdleme11h  40929  cdlemednuN  40963  cdleme20j  40981  cdleme20k  40982  cdleme21at  40991  cdleme35f  41117  cdlemg11b  41305  dia2dimlem1  41727  dihmeetlem3N  41968  dihmeetlem15N  41984  dochsnnz  42113  dochexmidlem1  42123  dochexmidlem7  42129  mapdindp3  42385  fltne  43267  pellexlem1  43447  dfac21  43684  pm13.14  45010  uzlidlring  48888  suppdm  49174