Theorem necon3bbid 2992

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

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

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 2956

This theorem is used by:  necon1abid  2993  necon3bid  2999  eldifsn  4747  php  9223  xmullem2  13396  fzdif1  13740  seqcoll2  14611  sgnneg  15254  cnpart  15408  rlimrecl  15748  ncoprmgcdne1b  16826  prmrp  16889  4sqlem17  17140  mrieqvd  17813  mrieqv2d  17814  pltval  18505  latnlemlt  18647  latnle  18648  degenmgm2nfun  19140  odnncl  19760  gexnnod  19803  sylow1lem1  19813  slwpss  19827  lssnle  19889  nzrunit  20776  isdrng4  20993  imadrhmcl  21055  lspsnne1  21396  pridln1  21625  cnsubrg  21734  psrridm  22271  mhpmulcl  22471  cmpfi  23727  hausdiag  23965  txhaus  23967  isusp  24581  recld2  25135  metdseq0  25175  i1f1lem  26011  aaliou2b  26669  dvloglem  26977  logf1o2  26979  lgsne0  27663  lgsqr  27679  2sqlem7  27752  ostth3  27966  tglngne  29014  tgelrnln  29099  eucrct2eupth  30847  norm1exi  31853  atnemeq0  32980  opeldifid  33236  arginv  33382  unitnz  33842  mxidln1  34034  ssmxidllem  34041  rprmnz  34095  ply1unit  34150  ply1dg3rt0irred  34159  constrrtll  34406  qtophaus  34511  ordtconnlem1  34599  elzrhunit  34652  subfacp1lem6  36019  maxidln1  39054  smprngopr  39062  lsatnem0  40178  atncmp  40445  atncvrN  40448  cdlema2N  40925  lhpmatb  41164  lhpat3  41179  cdleme3  41370  cdleme7  41382  cdlemg27b  41829  dvh2dimatN  42573  dvh2dim  42578  dochexmidlem1  42593  dochfln0  42610  dvrelog2b  43192  aks6d1c2p2  43245  hashscontpow  43248  rspcsbnea  43257