Theorem necon3bbid 2860

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon1abid  2861  necon3bid  2867  eldifsn  4350  php  8185  xmullem2  12133  seqcoll2  13287  cnpart  14024  rlimrecl  14355  ncoprmgcdne1b  15410  prmrp  15471  4sqlem17  15712  mrieqvd  16345  mrieqv2d  16346  pltval  17007  latnlemlt  17131  latnle  17132  odnncl  18010  gexnnod  18049  sylow1lem1  18059  slwpss  18073  lssnle  18133  lspsnne1  19165  nzrunit  19315  psrridm  19452  cnsubrg  19854  cmpfi  21259  hausdiag  21496  txhaus  21498  isusp  22112  recld2  22664  metdseq0  22704  i1f1lem  23501  aaliou2b  24141  dvloglem  24439  logf1o2  24441  lgsne0  25105  lgsqr  25121  2sqlem7  25194  ostth3  25372  tglngne  25490  tgelrnln  25570  eucrct2eupth  27223  norm1exi  28235  atnemeq0  29364  opeldifid  29538  qtophaus  30031  ordtconnlem1  30098  elzrhunit  30151  sgnneg  30730  subfacp1lem6  31293  maxidln1  33973  smprngopr  33981  lsatnem0  34650  atncmp  34917  atncvrN  34920  cdlema2N  35396  lhpmatb  35635  lhpat3  35650  cdleme3  35842  cdleme7  35854  cdlemg27b  36301  dvh2dimatN  37046  dvh2dim  37051  dochexmidlem1  37066  dochfln0  37083