Theorem necom 2994

Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)

Assertion

Ref	Expression
necom	⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 2739	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3bii 2993	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Syntax hints:   ↔ wb 205   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  necomi  2995  necomd  2996  0pss  4443  disjtp2  4719  difprsn1  4802  difprsn2  4803  prproe  4905  fndmdifcom  7041  fvpr1g  7184  fvpr2g  7185  fvpr1OLD  7188  fvpr2OLD  7190  fvtp1  7192  fvtp2  7193  fvtp3  7194  fvtp1g  7195  fvtp2g  7196  fvtp3g  7197  dff14b  7266  f12dfv  7267  f13dfv  7268  orduniorsuc  7814  kmlem3  10143  kmlem4  10144  ac6num  10470  leltne  11299  nn0lt2  12621  xrleltne  13120  fzofzim  13675  elfznelfzo  13733  elfznelfzob  13734  fleqceilz  13815  hashdifpr  14371  hashgt12el  14378  hashgt12el2  14379  hashgt23el  14380  cshw0  14740  cshwn  14743  isprm2lem  16614  prm2orodd  16624  cshwsdisj  17028  sgrp2nmndlem5  18806  f1omvdconj  19308  pmtrprfv3  19316  pmtr3ncomlem1  19335  dmdprdd  19863  cnfldfunALT  20949  xrsdsreclblem  20983  xrsdsreclb  20984  ordthaus  22879  hmphindis  23292  angpined  26324  nosgnn0  27150  noextendlt  27161  nosepne  27172  nosepdm  27176  nosupbnd2lem1  27207  noinfbnd2lem1  27222  noetasuplem4  27228  funvtxval0  28264  snstrvtxval  28286  snstriedgval  28287  nbgrsym  28609  nb3grprlem2  28627  nb3grpr  28628  cusgredg  28670  cplgr3v  28681  1egrvtxdg0  28757  usgr2pthlem  29009  usgr2pth0  29011  2pthdlem1  29173  clwlkclwwlklem2a4  29239  uhgr3cyclex  29424  eupth2lem3lem4  29473  frcond1  29508  frcond4  29512  frgr3v  29517  3vfriswmgr  29520  2pthfrgr  29526  3cyclfrgrrn1  29527  n4cyclfrgr  29533  frgrnbnb  29535  frgrwopreglem4a  29552  ch0pss  30685  pmtrprfv2  32236  esumcvgre  33077  bnj563  33742  cusgredgex2  34101  cvmsdisj  34249  fmlaomn0  34369  ex-sategoelel  34400  btwnouttr  34984  fscgr  35040  linecom  35110  linerflx2  35111  poimirlem25  36501  divrngidl  36884  lcvbr3  37881  opltn0  38048  atlltn0  38164  2dim  38329  ps-2  38337  islln3  38369  llnexatN  38380  4atlem11  38468  isline4N  38636  lhpex2leN  38872  cdleme48gfv  39396  60gcd7e1  40858  dvrelogpow2b  40921  aks4d1p1p4  40924  aks6d1c2p2  40945  fsuppind  41159  onov0suclim  42009  oenassex  42053  pr2eldif2  42291  pimxrneun  44185  icccncfext  44589  fourierdlem42  44851  icceuelpartlem  46089  ichnreuop  46126  paireqne  46165  oddprmALTV  46341  rrx2pnedifcoorneor  47355  rrx2linest  47381