Theorem necon3bd 2973

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  necon2ad  2974  nssne1  3975  nssne2  3976  disjne  4411  nbrne1  5127  nbrne2  5128  peano5  7929  oeeui  8639  domdifsn  9107  ac6sfi  9303  inf3lem2  9657  cnfcom3lem  9731  dfac9  10242  fin23lem21  10444  1re  11335  dedekindle  11501  zneo  12809  modirr  14112  sqrmo  15447  reusq0  15661  pc2dvds  17086  pcadd  17096  oddprmdvds  17110  4sqlem11  17162  latnlej  18659  sylow2blem3  19866  irredn0  20683  irredn1  20686  isnzr2  20798  lssvneln0  21257  lspsnne2  21426  lspfixed  21436  lspindpi  21440  lsmcv  21449  lspsolv  21451  coe1tmmul  22626  dfac14  23967  fbdmn0  24183  filufint  24269  flimfnfcls  24377  alexsubALTlem2  24397  evth  25310  cphsqrtcl2  25537  ovolicc2lem4  25871  lhop1lem  26363  lhop1  26364  lhop2  26365  lhop  26366  deg1add  26451  abelthlem2  26789  logcnlem2  27001  angpined  27188  asinneg  27244  dmgmaddn0  27380  lgsne0  27692  lgsqr  27708  lgsquadlem2  27738  lgsquadlem3  27739  fltne  28005  axlowdimlem17  29566  spansncvi  32284  tgextalem1inag  33100  argcj  33410  constrrecl  34471  zarcmplem  34583  nelscottrankgt  35833  broutsideof2  37065  unblimceq0lem  37550  poimirlem28  38758  dvasin  38814  dvacos  38815  nninfnub  38877  dvrunz  39080  lsatcvatlem  40298  lkrlsp2  40352  opnlen0  40437  2llnne2N  40657  lnnat  40676  llnn0  40765  lplnn0N  40796  lplnllnneN  40805  llncvrlpln2  40806  llncvrlpln  40807  lvoln0N  40840  lplncvrlvol2  40864  lplncvrlvol  40865  dalempnes  40900  dalemqnet  40901  dalemcea  40909  dalem3  40913  cdlema1N  41040  cdlemb  41043  paddasslem5  41073  llnexchb2lem  41117  osumcllem4N  41208  pexmidlem1N  41219  lhp2lt  41250  lhp2atne  41283  lhp2at0ne  41285  4atexlemunv  41315  4atexlemex2  41320  trlne  41434  trlval4  41437  cdlemc4  41443  cdleme11dN  41511  cdleme11h  41515  cdlemednuN  41549  cdleme20j  41567  cdleme20k  41568  cdleme21at  41577  cdleme35f  41703  cdlemg11b  41891  dia2dimlem1  42313  dihmeetlem3N  42554  dihmeetlem15N  42570  dochsnnz  42699  dochexmidlem1  42709  dochexmidlem7  42715  mapdindp3  42971  pellexlem1  44029  dfac21  44261  pm13.14  45585  uzlidlring  49537  suppdm  49827