Theorem necon3abid 2995

Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)

Hypothesis

Ref	Expression
necon3abid.1	⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))

Assertion

Ref	Expression
necon3abid	⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Proof of Theorem necon3abid

Step	Hyp	Ref	Expression
1		df-ne 2960	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 321	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	bitrid 286	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = 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:  necon3bbid  2996  necon2abid  3001  prneimg2  4813  prnesn  4818  foconst  6836  fndmdif  7067  suppsnop  8226  tz7.48lem  8481  om00el  8615  oeoa  8637  cardsdom2  10099  mulne0b  11987  crne0  12343  expneg  14242  hashsdom  14555  prprrab  14648  gcdn0gt0  16722  cncongr2  16875  pltval3  18543  mulgnegnn  19326  domnmuln0  20994  drngmulne0  21052  lvecvsn0  21420  mvrf1  22326  connsub  23772  pthaus  23990  xkohaus  24005  bndth  25312  lebnumlem1  25315  dvcobr  26299  dvcnvlem  26329  mdegle0  26428  coemulhi  26606  vieta1lem1  26666  vieta1lem2  26667  aalioulem2  26693  cosne0  26890  atandm3  27239  wilthlem2  27429  issqf  27496  mumullem2  27540  dchrptlem3  27626  lgseisenlem3  27737  mulsne0bd  28605  brbtwn2  29516  colinearalg  29521  vdn0conngrumgrv2  30830  vdgn1frgrv2  30930  nmlno0lem  31428  nmlnop0iALT  32630  atcvat2i  33022  elq2  33476  divnumden2  33480  domnmuln0rd  33914  lindssn  34017  mxidlirredi  34080  mxidlirred  34081  deg1prod  34198  fedgmullem2  34345  minplyirred  34426  cos9thpiminplylem3  34499  bnj1542  35570  bnj1253  35730  ptrecube  38743  poimirlem13  38756  ecinn0  39488  llnexchb2  41129  cdlemb3  41866  aks6d1c2p2  43372  aks6d1c6lem3  43425  fsuppind  43822  rencldnfilem  44031  qirropth  44119  binomcxplemfrat  45538  binomcxplemradcnv  45539  mod2addne  48655  odz2prm2pw  48863