Theorem necom 2995

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 205   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  necomi  2996  necomd  2997  0pss  4445  disjtp2  4721  difprsn1  4804  difprsn2  4805  prproe  4907  fndmdifcom  7045  fvpr1g  7188  fvpr2g  7189  fvpr1OLD  7192  fvpr2OLD  7194  fvtp1  7196  fvtp2  7197  fvtp3  7198  fvtp1g  7199  fvtp2g  7200  fvtp3g  7201  dff14b  7270  f12dfv  7271  f13dfv  7272  orduniorsuc  7818  kmlem3  10147  kmlem4  10148  ac6num  10474  leltne  11303  nn0lt2  12625  xrleltne  13124  fzofzim  13679  elfznelfzo  13737  elfznelfzob  13738  fleqceilz  13819  hashdifpr  14375  hashgt12el  14382  hashgt12el2  14383  hashgt23el  14384  cshw0  14744  cshwn  14747  isprm2lem  16618  prm2orodd  16628  cshwsdisj  17032  sgrp2nmndlem5  18810  f1omvdconj  19314  pmtrprfv3  19322  pmtr3ncomlem1  19341  dmdprdd  19869  cnfldfunALT  20957  xrsdsreclblem  20991  xrsdsreclb  20992  ordthaus  22888  hmphindis  23301  angpined  26335  nosgnn0  27161  noextendlt  27172  nosepne  27183  nosepdm  27187  nosupbnd2lem1  27218  noinfbnd2lem1  27233  noetasuplem4  27239  funvtxval0  28275  snstrvtxval  28297  snstriedgval  28298  nbgrsym  28620  nb3grprlem2  28638  nb3grpr  28639  cusgredg  28681  cplgr3v  28692  1egrvtxdg0  28768  usgr2pthlem  29020  usgr2pth0  29022  2pthdlem1  29184  clwlkclwwlklem2a4  29250  uhgr3cyclex  29435  eupth2lem3lem4  29484  frcond1  29519  frcond4  29523  frgr3v  29528  3vfriswmgr  29531  2pthfrgr  29537  3cyclfrgrrn1  29538  n4cyclfrgr  29544  frgrnbnb  29546  frgrwopreglem4a  29563  ch0pss  30698  pmtrprfv2  32249  esumcvgre  33089  bnj563  33754  cusgredgex2  34113  cvmsdisj  34261  fmlaomn0  34381  ex-sategoelel  34412  btwnouttr  34996  fscgr  35052  linecom  35122  linerflx2  35123  poimirlem25  36513  divrngidl  36896  lcvbr3  37893  opltn0  38060  atlltn0  38176  2dim  38341  ps-2  38349  islln3  38381  llnexatN  38392  4atlem11  38480  isline4N  38648  lhpex2leN  38884  cdleme48gfv  39408  60gcd7e1  40870  dvrelogpow2b  40933  aks4d1p1p4  40936  aks6d1c2p2  40957  fsuppind  41162  onov0suclim  42024  oenassex  42068  pr2eldif2  42306  pimxrneun  44199  icccncfext  44603  fourierdlem42  44865  icceuelpartlem  46103  ichnreuop  46140  paireqne  46179  oddprmALTV  46355  rrx2pnedifcoorneor  47402  rrx2linest  47428