Theorem necon3bbid 2968

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

Hypothesis

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

Assertion

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

Proof of Theorem necon3bbid

Step	Hyp	Ref	Expression
1		necon3bbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))
2	1	bicomd 222	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	necon3abid 2967	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
4	3	bicomd 222	1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1534   ≠ wne 2930

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 206  df-ne 2931

This theorem is referenced by:  necon1abid  2969  necon3bid  2975  eldifsn  4785  php  9237  phpOLD  9249  xmullem2  13292  seqcoll2  14479  cnpart  15240  rlimrecl  15577  ncoprmgcdne1b  16646  prmrp  16708  4sqlem17  16958  mrieqvd  17646  mrieqv2d  17647  pltval  18352  latnlemlt  18492  latnle  18493  odnncl  19539  gexnnod  19582  sylow1lem1  19592  slwpss  19606  lssnle  19668  nzrunit  20502  imadrhmcl  20772  lspsnne1  21094  cnsubrg  21420  psrridm  21968  mhpmulcl  22139  cmpfi  23400  hausdiag  23637  txhaus  23639  isusp  24254  recld2  24818  metdseq0  24858  i1f1lem  25706  aaliou2b  26366  dvloglem  26672  logf1o2  26674  lgsne0  27361  lgsqr  27377  2sqlem7  27450  ostth3  27664  tglngne  28474  tgelrnln  28554  eucrct2eupth  30175  norm1exi  31180  atnemeq0  32307  opeldifid  32519  unitnz  33109  isdrng4  33152  pridln1  33324  mxidln1  33347  ssmxidllem  33354  rprmnz  33401  ply1unit  33453  ply1dg3rt0irred  33460  constrrtll  33604  qtophaus  33664  ordtconnlem1  33752  elzrhunit  33807  sgnneg  34387  subfacp1lem6  35026  maxidln1  37758  smprngopr  37766  lsatnem0  38756  atncmp  39023  atncvrN  39026  cdlema2N  39504  lhpmatb  39743  lhpat3  39758  cdleme3  39949  cdleme7  39961  cdlemg27b  40408  dvh2dimatN  41152  dvh2dim  41157  dochexmidlem1  41172  dochfln0  41189  dvrelog2b  41778  aks6d1c2p2  41831  hashscontpow  41834  rspcsbnea  41843  nna4b4nsq  42350