Theorem gtneii 11256

Description: 'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.)

Hypotheses

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

Assertion

Ref	Expression
gtneii	⊢ 𝐵 ≠ 𝐴

Proof of Theorem gtneii

Step	Hyp	Ref	Expression
1		lt.1	. 2 ⊢ 𝐴 ∈ ℝ
2		ltneii.2	. 2 ⊢ 𝐴 < 𝐵
3		ltne 11241	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
4	1, 2, 3	mp2an 698	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ∈ wcel 2119   ≠ wne 2935   class class class wbr 5079  ℝcr 11035   < clt 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-pre-lttri 11110  ax-pre-lttrn 11111

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182

This theorem is referenced by:  ltneii  11257  fztpval  13538  tpf1ofv2  14458  geo2sum  15836  bpoly4  16022  ene1  16175  3dvds  16298  3lcm2e6  16700  starvndxnbasendx  17265  starvndxnplusgndx  17266  starvndxnmulrndx  17267  scandxnbasendx  17277  scandxnplusgndx  17278  scandxnmulrndx  17279  vscandxnbasendx  17282  vscandxnplusgndx  17283  vscandxnmulrndx  17284  vscandxnscandx  17285  ipndxnbasendx  17293  ipndxnplusgndx  17294  ipndxnmulrndx  17295  tsetndxnbasendx  17317  tsetndxnplusgndx  17318  tsetndxnmulrndx  17319  tsetndxnstarvndx  17320  slotstnscsi  17321  plendxnbasendx  17331  plendxnplusgndx  17332  plendxnmulrndx  17333  plendxnscandx  17334  plendxnvscandx  17335  dsndxnbasendx  17350  dsndxnplusgndx  17351  dsndxnmulrndx  17352  slotsdnscsi  17353  dsndxntsetndx  17354  unifndxnbasendx  17360  unifndxntsetndx  17361  psgnodpmr  21572  logbrec  26771  2logb9irr  26784  2logb3irr  26786  log2le1  26939  2lgsoddprmlem3a  27398  2lgsoddprmlem3b  27399  2lgsoddprmlem3c  27400  2lgsoddprmlem3d  27401  slotsinbpsd  28534  slotslnbpsd  28535  lngndxnitvndx  28536  konigsberglem2  30348  ex-dif  30518  ex-in  30520  ex-pss  30523  ex-res  30536  sgnnbi  32937  sgnpbi  32938  dp20u  32963  dp20h  32964  dp2clq  32966  dp2lt10  32969  dp2lt  32970  dplti  32990  dpexpp1  32993  2sqr3nconstr  33972  cos9thpinconstrlem2  33981  ballotlemi1  34694  signswch  34752  itgexpif  34797  hgt750lemd  34839  hgt750lem  34842  fdc  38119  tan3rdpi  42836  asin1half  42841  areaquad  43668  stirlinglem4  46527  stirlinglem13  46536  stirlinglem14  46537  stirlingr  46540  dirker2re  46542  dirkerdenne0  46543  dirkerre  46545  dirkertrigeqlem1  46548  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem16  46573  fourierdlem21  46578  fourierdlem22  46579  fourierdlem66  46622  fourierdlem83  46639  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  etransclem46  46730  fmtnoprmfac2lem1  48051  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  usgrexmpl2trifr  48535  zlmodzxzldeplem  48996