Theorem gtneii 8115

Description: 'Less than' implies not equal. See also gtapii 8653 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)

Hypotheses

Ref	Expression
lt.1	|- A e. RR
ltneii.2	|- A < B

Assertion

Ref	Expression
gtneii	|- B =/= A

Proof of Theorem gtneii

Step	Hyp	Ref	Expression
1		lt.1	. 2 |- A e. RR
2		ltneii.2	. 2 |- A < B
3		ltne 8104	. 2 |- ( ( A e. RR /\ A < B ) -> B =/= A )
4	1, 2, 3	mp2an 426	1 |- B =/= A

Syntax hints:   e. wcel 2164   =/= wne 2364   class class class wbr 4029   RRcr 7871   < clt 8054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-pre-ltirr 7984

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-xp 4665  df-pnf 8056  df-mnf 8057  df-ltxr 8059

This theorem is referenced by:  ltneii  8116  ine0  8413  fztpval  10149  ene1  11928  3lcm2e6  12298  starvndxnbasendx  12759  starvndxnplusgndx  12760  starvndxnmulrndx  12761  scandxnbasendx  12771  scandxnplusgndx  12772  scandxnmulrndx  12773  vscandxnbasendx  12776  vscandxnplusgndx  12777  vscandxnmulrndx  12778  vscandxnscandx  12779  ipndxnbasendx  12789  ipndxnplusgndx  12790  ipndxnmulrndx  12791  tsetndxnbasendx  12808  tsetndxnplusgndx  12809  tsetndxnmulrndx  12810  tsetndxnstarvndx  12811  slotstnscsi  12812  plendxnbasendx  12822  plendxnplusgndx  12823  plendxnmulrndx  12824  plendxnscandx  12825  plendxnvscandx  12826  dsndxnbasendx  12833  dsndxnplusgndx  12834  dsndxnmulrndx  12835  slotsdnscsi  12836  dsndxntsetndx  12837  unifndxnbasendx  12843  unifndxntsetndx  12844  setsmsdsg  14648  2logb9irr  15103  2logb3irr  15105  2logb9irrap  15109