Theorem necon3bd 2943

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ 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 207  df-ne 2930

This theorem is referenced by:  necon2ad  2944  nssne1  3993  nssne2  3994  disjne  4404  nbrne1  5112  nbrne2  5113  peano5  7829  oeeui  8523  domdifsn  8980  ac6sfi  9175  inf3lem2  9526  cnfcom3lem  9600  dfac9  10035  fin23lem21  10237  1re  11119  dedekindle  11284  zneo  12562  modirr  13851  sqrmo  15160  reusq0  15374  pc2dvds  16793  pcadd  16803  oddprmdvds  16817  4sqlem11  16869  latnlej  18364  sylow2blem3  19536  irredn0  20343  irredn1  20346  isnzr2  20435  lssvneln0  20887  lspsnne2  21057  lspfixed  21067  lspindpi  21071  lsmcv  21080  lspsolv  21082  coe1tmmul  22192  dfac14  23534  fbdmn0  23750  filufint  23836  flimfnfcls  23944  alexsubALTlem2  23964  evth  24886  cphsqrtcl2  25114  ovolicc2lem4  25449  lhop1lem  25946  lhop1  25947  lhop2  25948  lhop  25949  deg1add  26036  abelthlem2  26370  logcnlem2  26580  angpined  26768  asinneg  26824  dmgmaddn0  26961  lgsne0  27274  lgsqr  27290  lgsquadlem2  27320  lgsquadlem3  27321  axlowdimlem17  28938  spansncvi  31634  argcj  32736  constrrecl  33803  zarcmplem  33915  broutsideof2  36187  unblimceq0lem  36571  poimirlem28  37709  dvasin  37765  dvacos  37766  nninfnub  37812  dvrunz  38015  lsatcvatlem  39169  lkrlsp2  39223  opnlen0  39308  2llnne2N  39528  lnnat  39547  llnn0  39636  lplnn0N  39667  lplnllnneN  39676  llncvrlpln2  39677  llncvrlpln  39678  lvoln0N  39711  lplncvrlvol2  39735  lplncvrlvol  39736  dalempnes  39771  dalemqnet  39772  dalemcea  39780  dalem3  39784  cdlema1N  39911  cdlemb  39914  paddasslem5  39944  llnexchb2lem  39988  osumcllem4N  40079  pexmidlem1N  40090  lhp2lt  40121  lhp2atne  40154  lhp2at0ne  40156  4atexlemunv  40186  4atexlemex2  40191  trlne  40305  trlval4  40308  cdlemc4  40314  cdleme11dN  40382  cdleme11h  40386  cdlemednuN  40420  cdleme20j  40438  cdleme20k  40439  cdleme21at  40448  cdleme35f  40574  cdlemg11b  40762  dia2dimlem1  41184  dihmeetlem3N  41425  dihmeetlem15N  41441  dochsnnz  41570  dochexmidlem1  41580  dochexmidlem7  41586  mapdindp3  41842  fltne  42763  pellexlem1  42947  dfac21  43184  pm13.14  44527  uzlidlring  48360  suppdm  48636