Theorem ltneii 11294

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 11293	. 2 ⊢ 𝐵 ≠ 𝐴
4	3	necomi 2980	1 ⊢ 𝐴 ≠ 𝐵

Syntax hints:   ∈ wcel 2109   ≠ wne 2926   class class class wbr 5110  ℝcr 11074   < clt 11215

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-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220

This theorem is referenced by:  1ne2  12396  f1oun2prg  14890  geo2sum  15846  3dvds  16308  basendxnplusgndx  17257  basendxnmulrndx  17266  plusgndxnmulrndx  17267  slotsdifipndx  17305  slotsdifplendx  17345  basendxnocndx  17353  plendxnocndx  17354  slotsdifdsndx  17364  slotsdifunifndx  17371  slotsbhcdif  17385  slotsdifplendx2  17386  slotsdifocndx  17387  ppiub  27122  2lgslem3  27322  2lgslem4  27324  addsq2nreurex  27362  basendxnedgfndx  28929  structvtxvallem  28954  usgrexmpldifpr  29192  upgr4cycl4dv4e  30121  konigsbergiedgw  30184  konigsberglem3  30190  konigsberglem5  30192  ex-dif  30359  ex-id  30370  ex-fv  30379  ex-mod  30385  9p10ne21  30406  evl1deg3  33554  2sqr3minply  33777  rabren3dioph  42810  xrlexaddrp  45355  fourierdlem102  46213  fourierdlem114  46225  fouriersw  46236  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2trifr  48032  zlmodzxznm  48490  2p2ne5  49791