Theorem necon3bbid 2970

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  necon1abid  2971  necon3bid  2977  eldifsn  4730  php  9132  xmullem2  13206  fzdif1  13548  seqcoll2  14416  cnpart  15191  rlimrecl  15531  ncoprmgcdne1b  16608  prmrp  16671  4sqlem17  16921  mrieqvd  17593  mrieqv2d  17594  pltval  18285  latnlemlt  18427  latnle  18428  odnncl  19509  gexnnod  19552  sylow1lem1  19562  slwpss  19576  lssnle  19638  nzrunit  20490  imadrhmcl  20763  lspsnne1  21105  cnsubrg  21415  psrridm  21950  mhpmulcl  22124  cmpfi  23382  hausdiag  23619  txhaus  23621  isusp  24235  recld2  24789  metdseq0  24829  i1f1lem  25665  aaliou2b  26320  dvloglem  26628  logf1o2  26630  lgsne0  27317  lgsqr  27333  2sqlem7  27406  ostth3  27620  tglngne  28637  tgelrnln  28717  eucrct2eupth  30335  norm1exi  31341  atnemeq0  32468  opeldifid  32689  arginv  32840  sgnneg  32926  unitnz  33320  isdrng4  33376  pridln1  33523  mxidln1  33546  ssmxidllem  33553  rprmnz  33600  ply1unit  33655  ply1dg3rt0irred  33664  constrrtll  33896  qtophaus  34001  ordtconnlem1  34089  elzrhunit  34142  subfacp1lem6  35388  maxidln1  38376  smprngopr  38384  lsatnem0  39502  atncmp  39769  atncvrN  39772  cdlema2N  40249  lhpmatb  40488  lhpat3  40503  cdleme3  40694  cdleme7  40706  cdlemg27b  41153  dvh2dimatN  41897  dvh2dim  41902  dochexmidlem1  41917  dochfln0  41934  dvrelog2b  42516  aks6d1c2p2  42569  hashscontpow  42572  rspcsbnea  42581  nna4b4nsq  43104