Theorem necom 3014

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

Assertion

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

Proof of Theorem necom

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

This proof depends on syntax axioms:   ↔ wb 209   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ne 2962

This theorem is used by:  necomi  3015  necomd  3016  dfdif3  4075  0pss  4370  iftrueb  4505  disjtp2  4687  difprsn1  4773  difprsn2  4774  prproe  4875  fndmdifcom  7045  fvpr1g  7195  fvpr2g  7196  fvtp1  7200  fvtp2  7201  fvtp3  7202  fvtp1g  7203  fvtp2g  7204  fvtp3g  7205  dff14b  7276  f12dfv  7282  f13dfv  7283  orduniorsuc  7835  kmlem3  10155  kmlem4  10156  ac6num  10481  leltne  11317  nn0lt2  12677  xrleltne  13188  fzofzim  13757  elfznelfzo  13821  elfznelfzob  13822  fleqceilz  13907  hashdifpr  14472  hashgt12el  14479  hashgt12el2  14480  hashgt23el  14481  hash7g  14543  cshw0  14857  cshwn  14860  isprm2lem  16764  prm2orodd  16774  cshwsdisj  17183  sgrp2nmndlem5  19022  f1omvdconj  19547  pmtrprfv3  19555  pmtr3ncomlem1  19574  dmdprdd  20102  cnfldfunALT  21574  xrsdsreclblem  21600  xrsdsreclb  21601  ordthaus  23578  hmphindis  23991  angpined  27032  nosgnn0  27859  noextendlt  27870  nosepne  27881  nosepdm  27885  nosupbnd2lem1  27916  noinfbnd2lem1  27931  noetasuplem4  27937  funvtxval0  29402  snstrvtxval  29424  snstriedgval  29425  nbgrsym  29750  nb3grprlem2  29768  nb3grpr  29769  cusgredg  29811  cplgr3v  29822  1egrvtxdg0  29898  usgr2pthlem  30149  usgr2pth0  30151  2pthdlem1  30316  clwlkclwwlklem2a4  30385  uhgr3cyclex  30570  eupth2lem3lem4  30619  frcond1  30654  frcond4  30658  frgr3v  30663  3vfriswmgr  30666  2pthfrgr  30672  3cyclfrgrrn1  30673  n4cyclfrgr  30679  frgrnbnb  30681  frgrwopreglem4a  30698  ch0pss  31834  pmtrprfv2  33439  esumcvgre  34512  bnj563  35164  cusgredgex2  35636  cvmsdisj  35783  fmlaomn0  35903  ex-sategoelel  35934  btwnouttr  36537  fscgr  36593  linecom  36663  linerflx2  36664  mh-inf3f1  37093  poimirlem25  38337  divrngidl  38720  lcvbr3  39838  opltn0  40005  atlltn0  40121  2dim  40285  ps-2  40293  islln3  40325  llnexatN  40336  4atlem11  40424  isline4N  40592  lhpex2leN  40828  cdleme48gfv  41352  60gcd7e1  42813  dvrelogpow2b  42876  aks4d1p1p4  42879  aks6d1c2p2  42927  fsuppind  43363  onov0suclim  44042  oenassex  44086  pr2eldif2  44322  pimxrneun  46243  icccncfext  46642  fourierdlem42  46904  sqrtnzqaa  47646  icceuelpartlem  48225  ichnreuop  48262  paireqne  48301  oddprmALTV  48493  rrx2pnedifcoorneor  49537  rrx2linest  49563