Theorem necon3bbid 2994

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 226	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	necon3abid 2993	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
4	3	bicomd 226	1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2957

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 2958

This theorem is used by:  necon1abid  2995  necon3bid  3001  eldifsn  4751  php  9204  xmullem2  13319  fzdif1  13662  seqcoll2  14532  sgnneg  15175  cnpart  15329  rlimrecl  15669  ncoprmgcdne1b  16744  prmrp  16807  4sqlem17  17057  mrieqvd  17730  mrieqv2d  17731  pltval  18422  latnlemlt  18564  latnle  18565  degenmgm2nfun  19056  odnncl  19676  gexnnod  19719  sylow1lem1  19729  slwpss  19743  lssnle  19805  nzrunit  20689  isdrng4  20906  imadrhmcl  20967  lspsnne1  21308  pridln1  21535  cnsubrg  21644  psrridm  22181  mhpmulcl  22381  cmpfi  23637  hausdiag  23875  txhaus  23877  isusp  24491  recld2  25045  metdseq0  25085  i1f1lem  25921  aaliou2b  26577  dvloglem  26886  logf1o2  26888  lgsne0  27572  lgsqr  27588  2sqlem7  27661  ostth3  27875  tglngne  28893  tgelrnln  28978  eucrct2eupth  30726  norm1exi  31732  atnemeq0  32859  opeldifid  33074  arginv  33220  unitnz  33680  mxidln1  33871  ssmxidllem  33878  rprmnz  33932  ply1unit  33987  ply1dg3rt0irred  33996  constrrtll  34243  qtophaus  34348  ordtconnlem1  34436  elzrhunit  34489  subfacp1lem6  35766  maxidln1  38796  smprngopr  38804  lsatnem0  39920  atncmp  40187  atncvrN  40190  cdlema2N  40667  lhpmatb  40906  lhpat3  40921  cdleme3  41112  cdleme7  41124  cdlemg27b  41571  dvh2dimatN  42315  dvh2dim  42320  dochexmidlem1  42335  dochfln0  42352  dvrelog2b  42934  aks6d1c2p2  42987  hashscontpow  42990  rspcsbnea  42999  nna4b4nsq  43508