Theorem gtneii 10733

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

Syntax hints:   ∈ wcel 2114   ≠ wne 3011   class class class wbr 5047  ℝcr 10517   < clt 10656

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 2792  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7442  ax-resscn 10575  ax-pre-lttri 10592  ax-pre-lttrn 10593

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 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3012  df-nel 3119  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3483  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-po 5455  df-so 5456  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-er 8270  df-en 8491  df-dom 8492  df-sdom 8493  df-pnf 10658  df-mnf 10659  df-ltxr 10661

This theorem is referenced by:  ltneii  10734  fztpval  12954  geo2sum  15209  bpoly4  15393  ene1  15543  3dvds  15660  3lcm2e6  16050  resslem  16535  rescco  17080  oppgtset  18458  symgvalstruct  18503  mgpsca  19224  mgptset  19225  mgpds  19227  cnfldfun  20535  psgnodpmr  20712  matsca  21002  matvsca  21003  tuslem  22854  setsmsds  23064  tngds  23235  logbrec  25341  2logb9irr  25354  2logb3irr  25356  log2le1  25509  2lgsoddprmlem3a  25967  2lgsoddprmlem3b  25968  2lgsoddprmlem3c  25969  2lgsoddprmlem3d  25970  konigsberglem2  28011  ex-dif  28181  ex-in  28183  ex-pss  28186  ex-res  28199  dp20u  30535  dp20h  30536  dp2clq  30538  dp2lt10  30541  dp2lt  30542  dplti  30562  dpexpp1  30565  oppgle  30621  resvvsca  30909  zlmds  31207  zlmtset  31208  ballotlemi1  31762  sgnnbi  31805  sgnpbi  31806  signswch  31833  itgexpif  31879  hgt750lemd  31921  hgt750lem  31924  fdc  35047  areaquad  39909  stirlinglem4  42447  stirlinglem13  42456  stirlinglem14  42457  stirlingr  42460  dirker2re  42462  dirkerdenne0  42463  dirkerre  42465  dirkertrigeqlem1  42468  dirkercncflem2  42474  dirkercncflem4  42476  fourierdlem16  42493  fourierdlem21  42498  fourierdlem22  42499  fourierdlem66  42542  fourierdlem83  42559  fourierdlem103  42579  fourierdlem104  42580  sqwvfoura  42598  sqwvfourb  42599  fourierswlem  42600  fouriersw  42601  etransclem46  42650  fmtnoprmfac2lem1  43808  zlmodzxzldeplem  44633