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 1569   ≠ 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  4752  php  9189  xmullem2  13297  fzdif1  13640  seqcoll2  14509  sgnneg  15144  cnpart  15298  rlimrecl  15638  ncoprmgcdne1b  16714  prmrp  16777  4sqlem17  17027  mrieqvd  17700  mrieqv2d  17701  pltval  18392  latnlemlt  18534  latnle  18535  odnncl  19621  gexnnod  19664  sylow1lem1  19674  slwpss  19688  lssnle  19750  nzrunit  20633  isdrng4  20850  imadrhmcl  20911  lspsnne1  21252  pridln1  21479  cnsubrg  21588  psrridm  22123  mhpmulcl  22323  cmpfi  23576  hausdiag  23813  txhaus  23815  isusp  24429  recld2  24983  metdseq0  25023  i1f1lem  25859  aaliou2b  26515  dvloglem  26824  logf1o2  26826  lgsne0  27510  lgsqr  27526  2sqlem7  27599  ostth3  27813  tglngne  28830  tgelrnln  28914  eucrct2eupth  30607  norm1exi  31613  atnemeq0  32740  opeldifid  32955  arginv  33103  unitnz  33567  mxidln1  33758  ssmxidllem  33765  rprmnz  33819  ply1unit  33874  ply1dg3rt0irred  33883  constrrtll  34130  qtophaus  34235  ordtconnlem1  34323  elzrhunit  34376  subfacp1lem6  35685  maxidln1  38723  smprngopr  38731  lsatnem0  39847  atncmp  40114  atncvrN  40117  cdlema2N  40594  lhpmatb  40833  lhpat3  40848  cdleme3  41039  cdleme7  41051  cdlemg27b  41498  dvh2dimatN  42242  dvh2dim  42247  dochexmidlem1  42262  dochfln0  42279  dvrelog2b  42861  aks6d1c2p2  42914  hashscontpow  42917  rspcsbnea  42926  nna4b4nsq  43420