Theorem gtneii 11234

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 11219	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
4	1, 2, 3	mp2an 692	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ∈ wcel 2113   ≠ wne 2929   class class class wbr 5095  ℝcr 11014   < clt 11155

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-resscn 11072  ax-pre-lttri 11089  ax-pre-lttrn 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-er 8630  df-en 8878  df-dom 8879  df-sdom 8880  df-pnf 11157  df-mnf 11158  df-ltxr 11160

This theorem is referenced by:  ltneii  11235  fztpval  13490  tpf1ofv2  14409  geo2sum  15784  bpoly4  15970  ene1  16123  3dvds  16246  3lcm2e6  16647  starvndxnbasendx  17212  starvndxnplusgndx  17213  starvndxnmulrndx  17214  scandxnbasendx  17224  scandxnplusgndx  17225  scandxnmulrndx  17226  vscandxnbasendx  17229  vscandxnplusgndx  17230  vscandxnmulrndx  17231  vscandxnscandx  17232  ipndxnbasendx  17240  ipndxnplusgndx  17241  ipndxnmulrndx  17242  tsetndxnbasendx  17264  tsetndxnplusgndx  17265  tsetndxnmulrndx  17266  tsetndxnstarvndx  17267  slotstnscsi  17268  plendxnbasendx  17278  plendxnplusgndx  17279  plendxnmulrndx  17280  plendxnscandx  17281  plendxnvscandx  17282  dsndxnbasendx  17297  dsndxnplusgndx  17298  dsndxnmulrndx  17299  slotsdnscsi  17300  dsndxntsetndx  17301  unifndxnbasendx  17307  unifndxntsetndx  17308  psgnodpmr  21531  logbrec  26722  2logb9irr  26735  2logb3irr  26737  log2le1  26890  2lgsoddprmlem3a  27351  2lgsoddprmlem3b  27352  2lgsoddprmlem3c  27353  2lgsoddprmlem3d  27354  slotsinbpsd  28422  slotslnbpsd  28423  lngndxnitvndx  28424  konigsberglem2  30237  ex-dif  30407  ex-in  30409  ex-pss  30412  ex-res  30425  sgnnbi  32828  sgnpbi  32829  dp20u  32867  dp20h  32868  dp2clq  32870  dp2lt10  32873  dp2lt  32874  dplti  32894  dpexpp1  32897  2sqr3nconstr  33817  cos9thpinconstrlem2  33826  ballotlemi1  34539  signswch  34597  itgexpif  34642  hgt750lemd  34684  hgt750lem  34687  fdc  37808  tan3rdpi  42473  asin1half  42478  areaquad  43336  stirlinglem4  46202  stirlinglem13  46211  stirlinglem14  46212  stirlingr  46215  dirker2re  46217  dirkerdenne0  46218  dirkerre  46220  dirkertrigeqlem1  46223  dirkercncflem2  46229  dirkercncflem4  46231  fourierdlem16  46248  fourierdlem21  46253  fourierdlem22  46254  fourierdlem66  46297  fourierdlem83  46314  fourierdlem103  46334  fourierdlem104  46335  sqwvfoura  46353  sqwvfourb  46354  fourierswlem  46355  fouriersw  46356  etransclem46  46405  fmtnoprmfac2lem1  47693  usgrexmpl2nb3  48161  usgrexmpl2nb4  48162  usgrexmpl2nb5  48163  usgrexmpl2trifr  48164  zlmodzxzldeplem  48626