Theorem necom 2993

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 205   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2940

This theorem is referenced by:  necomi  2994  necomd  2995  0pss  4444  disjtp2  4720  difprsn1  4803  difprsn2  4804  prproe  4906  fndmdifcom  7044  fvpr1g  7190  fvpr2g  7191  fvpr1OLD  7194  fvpr2OLD  7196  fvtp1  7198  fvtp2  7199  fvtp3  7200  fvtp1g  7201  fvtp2g  7202  fvtp3g  7203  dff14b  7273  f12dfv  7274  f13dfv  7275  orduniorsuc  7822  kmlem3  10153  kmlem4  10154  ac6num  10480  leltne  11310  nn0lt2  12632  xrleltne  13131  fzofzim  13686  elfznelfzo  13744  elfznelfzob  13745  fleqceilz  13826  hashdifpr  14382  hashgt12el  14389  hashgt12el2  14390  hashgt23el  14391  cshw0  14751  cshwn  14754  isprm2lem  16625  prm2orodd  16635  cshwsdisj  17039  sgrp2nmndlem5  18852  f1omvdconj  19362  pmtrprfv3  19370  pmtr3ncomlem1  19389  dmdprdd  19917  cnfldfunALT  21246  xrsdsreclblem  21280  xrsdsreclb  21281  ordthaus  23208  hmphindis  23621  angpined  26676  nosgnn0  27504  noextendlt  27515  nosepne  27526  nosepdm  27530  nosupbnd2lem1  27561  noinfbnd2lem1  27576  noetasuplem4  27582  funvtxval0  28708  snstrvtxval  28730  snstriedgval  28731  nbgrsym  29053  nb3grprlem2  29071  nb3grpr  29072  cusgredg  29114  cplgr3v  29125  1egrvtxdg0  29201  usgr2pthlem  29453  usgr2pth0  29455  2pthdlem1  29617  clwlkclwwlklem2a4  29683  uhgr3cyclex  29868  eupth2lem3lem4  29917  frcond1  29952  frcond4  29956  frgr3v  29961  3vfriswmgr  29964  2pthfrgr  29970  3cyclfrgrrn1  29971  n4cyclfrgr  29977  frgrnbnb  29979  frgrwopreglem4a  29996  ch0pss  31131  pmtrprfv2  32685  esumcvgre  33553  bnj563  34218  cusgredgex2  34577  cvmsdisj  34725  fmlaomn0  34845  ex-sategoelel  34876  btwnouttr  35466  fscgr  35522  linecom  35592  linerflx2  35593  gg-cnfldfunALT  35645  poimirlem25  36977  divrngidl  37360  lcvbr3  38357  opltn0  38524  atlltn0  38640  2dim  38805  ps-2  38813  islln3  38845  llnexatN  38856  4atlem11  38944  isline4N  39112  lhpex2leN  39348  cdleme48gfv  39872  60gcd7e1  41337  dvrelogpow2b  41400  aks4d1p1p4  41403  aks6d1c2p2  41424  fsuppind  41625  onov0suclim  42487  oenassex  42531  pr2eldif2  42769  pimxrneun  44658  icccncfext  45062  fourierdlem42  45324  icceuelpartlem  46562  ichnreuop  46599  paireqne  46638  oddprmALTV  46814  rrx2pnedifcoorneor  47564  rrx2linest  47590