Theorem necom 2985

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2932

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  necomi  2986  necomd  2987  dfdif3  4092  0pss  4422  iftrueb  4513  disjtp2  4692  difprsn1  4776  difprsn2  4777  prproe  4881  fndmdifcom  7032  fvpr1g  7181  fvpr2g  7182  fvtp1  7186  fvtp2  7187  fvtp3  7188  fvtp1g  7189  fvtp2g  7190  fvtp3g  7191  dff14b  7263  f12dfv  7265  f13dfv  7266  orduniorsuc  7822  kmlem3  10165  kmlem4  10166  ac6num  10491  leltne  11322  nn0lt2  12654  xrleltne  13159  fzofzim  13724  elfznelfzo  13786  elfznelfzob  13787  fleqceilz  13869  hashdifpr  14431  hashgt12el  14438  hashgt12el2  14439  hashgt23el  14440  hash7g  14502  cshw0  14810  cshwn  14813  isprm2lem  16698  prm2orodd  16708  cshwsdisj  17116  sgrp2nmndlem5  18905  f1omvdconj  19425  pmtrprfv3  19433  pmtr3ncomlem1  19452  dmdprdd  19980  cnfldfunALT  21328  cnfldfunALTOLD  21341  xrsdsreclblem  21378  xrsdsreclb  21379  ordthaus  23320  hmphindis  23733  angpined  26790  nosgnn0  27620  noextendlt  27631  nosepne  27642  nosepdm  27646  nosupbnd2lem1  27677  noinfbnd2lem1  27692  noetasuplem4  27698  funvtxval0  28940  snstrvtxval  28962  snstriedgval  28963  nbgrsym  29288  nb3grprlem2  29306  nb3grpr  29307  cusgredg  29349  cplgr3v  29360  1egrvtxdg0  29437  usgr2pthlem  29691  usgr2pth0  29693  2pthdlem1  29858  clwlkclwwlklem2a4  29924  uhgr3cyclex  30109  eupth2lem3lem4  30158  frcond1  30193  frcond4  30197  frgr3v  30202  3vfriswmgr  30205  2pthfrgr  30211  3cyclfrgrrn1  30212  n4cyclfrgr  30218  frgrnbnb  30220  frgrwopreglem4a  30237  ch0pss  31372  pmtrprfv2  33045  esumcvgre  34068  bnj563  34720  cusgredgex2  35091  cvmsdisj  35238  fmlaomn0  35358  ex-sategoelel  35389  btwnouttr  35988  fscgr  36044  linecom  36114  linerflx2  36115  poimirlem25  37615  divrngidl  37998  lcvbr3  38987  opltn0  39154  atlltn0  39270  2dim  39435  ps-2  39443  islln3  39475  llnexatN  39486  4atlem11  39574  isline4N  39742  lhpex2leN  39978  cdleme48gfv  40502  60gcd7e1  41964  dvrelogpow2b  42027  aks4d1p1p4  42030  aks6d1c2p2  42078  fsuppind  42560  onov0suclim  43245  oenassex  43289  pr2eldif2  43526  pimxrneun  45463  icccncfext  45864  fourierdlem42  46126  icceuelpartlem  47397  ichnreuop  47434  paireqne  47473  oddprmALTV  47649  rrx2pnedifcoorneor  48644  rrx2linest  48670