Theorem necom 2979

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  necomi  2980  necomd  2981  dfdif3  4083  0pss  4413  iftrueb  4504  disjtp2  4683  difprsn1  4767  difprsn2  4768  prproe  4872  fndmdifcom  7018  fvpr1g  7167  fvpr2g  7168  fvtp1  7172  fvtp2  7173  fvtp3  7174  fvtp1g  7175  fvtp2g  7176  fvtp3g  7177  dff14b  7249  f12dfv  7251  f13dfv  7252  orduniorsuc  7808  kmlem3  10113  kmlem4  10114  ac6num  10439  leltne  11270  nn0lt2  12604  xrleltne  13112  fzofzim  13677  elfznelfzo  13740  elfznelfzob  13741  fleqceilz  13823  hashdifpr  14387  hashgt12el  14394  hashgt12el2  14395  hashgt23el  14396  hash7g  14458  cshw0  14766  cshwn  14769  isprm2lem  16658  prm2orodd  16668  cshwsdisj  17076  sgrp2nmndlem5  18863  f1omvdconj  19383  pmtrprfv3  19391  pmtr3ncomlem1  19410  dmdprdd  19938  cnfldfunALT  21286  cnfldfunALTOLD  21299  xrsdsreclblem  21336  xrsdsreclb  21337  ordthaus  23278  hmphindis  23691  angpined  26747  nosgnn0  27577  noextendlt  27588  nosepne  27599  nosepdm  27603  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetasuplem4  27655  funvtxval0  28949  snstrvtxval  28971  snstriedgval  28972  nbgrsym  29297  nb3grprlem2  29315  nb3grpr  29316  cusgredg  29358  cplgr3v  29369  1egrvtxdg0  29446  usgr2pthlem  29700  usgr2pth0  29702  2pthdlem1  29867  clwlkclwwlklem2a4  29933  uhgr3cyclex  30118  eupth2lem3lem4  30167  frcond1  30202  frcond4  30206  frgr3v  30211  3vfriswmgr  30214  2pthfrgr  30220  3cyclfrgrrn1  30221  n4cyclfrgr  30227  frgrnbnb  30229  frgrwopreglem4a  30246  ch0pss  31381  pmtrprfv2  33052  esumcvgre  34088  bnj563  34740  cusgredgex2  35117  cvmsdisj  35264  fmlaomn0  35384  ex-sategoelel  35415  btwnouttr  36019  fscgr  36075  linecom  36145  linerflx2  36146  poimirlem25  37646  divrngidl  38029  lcvbr3  39023  opltn0  39190  atlltn0  39306  2dim  39471  ps-2  39479  islln3  39511  llnexatN  39522  4atlem11  39610  isline4N  39778  lhpex2leN  40014  cdleme48gfv  40538  60gcd7e1  42000  dvrelogpow2b  42063  aks4d1p1p4  42066  aks6d1c2p2  42114  fsuppind  42585  onov0suclim  43270  oenassex  43314  pr2eldif2  43551  pimxrneun  45491  icccncfext  45892  fourierdlem42  46154  icceuelpartlem  47440  ichnreuop  47477  paireqne  47516  oddprmALTV  47692  rrx2pnedifcoorneor  48709  rrx2linest  48735