Theorem necon3bbid 2972

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon1abid  2973  necon3bid  2979  eldifsn  4726  php  9138  xmullem2  13215  fzdif1  13557  seqcoll2  14425  cnpart  15200  rlimrecl  15540  ncoprmgcdne1b  16617  prmrp  16680  4sqlem17  16930  mrieqvd  17602  mrieqv2d  17603  pltval  18294  latnlemlt  18436  latnle  18437  odnncl  19518  gexnnod  19561  sylow1lem1  19571  slwpss  19585  lssnle  19647  nzrunit  20503  imadrhmcl  20776  lspsnne1  21117  cnsubrg  21409  psrridm  21944  mhpmulcl  22144  cmpfi  23398  hausdiag  23635  txhaus  23637  isusp  24251  recld2  24805  metdseq0  24845  i1f1lem  25681  aaliou2b  26332  dvloglem  26637  logf1o2  26639  lgsne0  27323  lgsqr  27339  2sqlem7  27412  ostth3  27626  tglngne  28643  tgelrnln  28723  eucrct2eupth  30340  norm1exi  31346  atnemeq0  32473  opeldifid  32695  arginv  32846  sgnneg  32932  unitnz  33327  isdrng4  33386  pridln1  33533  mxidln1  33556  ssmxidllem  33563  rprmnz  33610  ply1unit  33665  ply1dg3rt0irred  33674  constrrtll  33922  qtophaus  34027  ordtconnlem1  34115  elzrhunit  34168  subfacp1lem6  35414  maxidln1  38412  smprngopr  38420  lsatnem0  39538  atncmp  39805  atncvrN  39808  cdlema2N  40285  lhpmatb  40524  lhpat3  40539  cdleme3  40730  cdleme7  40742  cdlemg27b  41189  dvh2dimatN  41933  dvh2dim  41938  dochexmidlem1  41953  dochfln0  41970  dvrelog2b  42552  aks6d1c2p2  42605  hashscontpow  42608  rspcsbnea  42617  nna4b4nsq  43111