Theorem ltneii 11416

Description: 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)

Hypotheses

Ref	Expression
lt.1	⊢ 𝐴 ∈ ℝ
ltneii.2	⊢ 𝐴 < 𝐵

Assertion

Ref	Expression
ltneii	⊢ 𝐴 ≠ 𝐵

Proof of Theorem ltneii

Step	Hyp	Ref	Expression
1		lt.1	. . 3 ⊢ 𝐴 ∈ ℝ
2		ltneii.2	. . 3 ⊢ 𝐴 < 𝐵
3	1, 2	gtneii 11415	. 2 ⊢ 𝐵 ≠ 𝐴
4	3	necomi 3010	1 ⊢ 𝐴 ≠ 𝐵

This proof depends on syntax axioms:   ∈ wcel 2145   ≠ wne 2956   class class class wbr 5103  ℝcr 11192   < clt 11336

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-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-pre-lttri 11267  ax-pre-lttrn 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341

This theorem is used by:  1ne2  12546  f1oun2prg  15061  geo2sum  16035  3dvds  16494  basendxnplusgndx  17451  basendxnmulrndx  17460  plusgndxnmulrndx  17461  slotsdifipndx  17499  slotsdifplendx  17539  basendxnocndx  17547  plendxnocndx  17548  slotsdifdsndx  17558  slotsdifunifndx  17565  slotsbhcdif  17579  slotsdifplendx2  17580  slotsdifocndx  17581  ppiub  27524  2lgslem3  27724  2lgslem4  27726  addsq2nreurex  27764  basendxnedgfndx  29566  structvtxvallem  29591  usgrexmpldifpr  29832  upgr4cycl4dv4e  30779  konigsbergiedgw  30842  konigsberglem3  30848  konigsberglem5  30850  ex-dif  31017  ex-id  31028  ex-fv  31037  ex-mod  31043  9p10ne21  31064  evl1deg3  34103  2sqr3minply  34405  rabren3dioph  43801  xrlexaddrp  46333  fourierdlem102  47187  fourierdlem114  47199  fouriersw  47210  sinnpoly  47910  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  usgrexmpl1lem  49088  usgrexmpl2lem  49093  usgrexmpl2nb0  49098  usgrexmpl2nb1  49099  usgrexmpl2nb2  49100  usgrexmpl2nb3  49101  usgrexmpl2nb4  49102  usgrexmpl2trifr  49104  gpg5edgnedg  49197  zlmodzxznm  49578  2p2ne5  50905  1ne3  50910  2ne3  50911  veronesev1lem  50942  veronesev2lem  50943  veronesev3lem  50944  veronesev4lem  50945  veronesev5lem  50946