Theorem ltneii 10753

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

Syntax hints:   ∈ wcel 2114   ≠ wne 3016   class class class wbr 5066  ℝcr 10536   < clt 10675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-pre-lttri 10611  ax-pre-lttrn 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-ltxr 10680

This theorem is referenced by:  1ne2  11846  f1oun2prg  14279  geo2sum  15229  3dvds  15680  plusgndxnmulrndx  16617  basendxnmulrndx  16618  slotsbhcdif  16693  oppchomfval  16984  oppcbas  16988  rescbas  17099  rescabs  17103  odubas  17743  opprlem  19378  rmodislmod  19702  srasca  19953  sravsca  19954  opsrbaslem  20258  cnfldfun  20557  zlmlem  20664  zlmsca  20668  znbaslem  20685  thlbas  20840  thlle  20841  tuslem  22876  setsmsbas  23085  tnglem  23249  ppiub  25780  2lgslem3  25980  2lgslem4  25982  addsq2nreurex  26020  ttgval  26661  ttglem  26662  slotsbaseefdif  26780  structvtxvallem  26805  usgrexmpldifpr  27040  upgr4cycl4dv4e  27964  konigsbergiedgw  28027  konigsberglem3  28033  konigsberglem5  28035  ex-dif  28202  ex-id  28213  ex-fv  28222  ex-mod  28228  9p10ne21  28249  resvbas  30905  resvplusg  30906  resvmulr  30908  hlhilslem  39089  rabren3dioph  39432  xrlexaddrp  41640  fourierdlem102  42513  fourierdlem114  42525  fouriersw  42536  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  zlmodzxznm  44572  2p2ne5  44919