Theorem necon3bbid 2996

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

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

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 2960

This theorem is used by:  necon1abid  2997  necon3bid  3003  eldifsn  4748  php  9250  xmullem2  13422  fzdif1  13766  seqcoll2  14637  sgnneg  15282  cnpart  15436  rlimrecl  15776  ncoprmgcdne1b  16854  prmrp  16917  4sqlem17  17168  mrieqvd  17841  mrieqv2d  17842  pltval  18533  latnlemlt  18675  latnle  18676  degenmgm2nfun  19168  odnncl  19789  gexnnod  19832  sylow1lem1  19842  slwpss  19856  lssnle  19918  nzrunit  20805  isdrng4  21022  imadrhmcl  21084  lspsnne1  21425  pridln1  21654  cnsubrg  21763  psrridm  22300  mhpmulcl  22500  cmpfi  23756  hausdiag  23994  txhaus  23996  isusp  24610  recld2  25164  metdseq0  25204  i1f1lem  26040  aaliou2b  26698  dvloglem  27006  logf1o2  27008  lgsne0  27692  lgsqr  27708  2sqlem7  27781  ostth3  27995  tglngne  29043  tgelrnln  29128  eucrct2eupth  30876  norm1exi  31882  atnemeq0  33009  opeldifid  33265  arginv  33409  unitnz  33869  mxidln1  34061  ssmxidllem  34068  rprmnz  34122  ply1unit  34177  ply1dg3rt0irred  34186  constrrtll  34433  qtophaus  34538  ordtconnlem1  34626  elzrhunit  34679  subfacp1lem6  36117  maxidln1  39170  smprngopr  39178  lsatnem0  40294  atncmp  40561  atncvrN  40564  cdlema2N  41041  lhpmatb  41280  lhpat3  41295  cdleme3  41486  cdleme7  41498  cdlemg27b  41945  dvh2dimatN  42689  dvh2dim  42694  dochexmidlem1  42709  dochfln0  42726  dvrelog2b  43308  aks6d1c2p2  43361  hashscontpow  43364  rspcsbnea  43373