Theorem ltned 11273

Description: 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltned.2	⊢ (𝜑 → 𝐴 < 𝐵)

Assertion

Ref	Expression
ltned	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem ltned

Step	Hyp	Ref	Expression
1		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltned.2	. . 3 ⊢ (𝜑 → 𝐴 < 𝐵)
3	1, 2	gtned 11272	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
4	3	necomd 2988	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933   class class class wbr 5086  ℝcr 11028   < clt 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  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 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  fzodisjsn  13643  fzone1  13730  modsumfzodifsn  13897  seqf1olem1  13994  nprm  16648  4sqlem10  16909  4sqlem17  16923  pgpfaclem2  20050  fvmptnn04ifb  22826  dvferm2lem  25963  lhop2  25992  ftc1lem5  26017  deg1tmle  26093  plyeq0lem  26185  aaliou3lem7  26326  dvloglem  26625  rtprmirr  26737  isosctrlem1  26795  bndatandm  26906  vma1  27143  rplogsumlem2  27462  rpvmasumlem  27464  axlowdimlem13  29037  axlowdimlem16  29040  strlem6  32342  hstrlem6  32350  pmtrto1cl  33175  psgnfzto1stlem  33176  cycpmrn  33219  drngidlhash  33509  prmidl0  33525  krull  33554  esplyfval2  33724  esplyfval3  33731  cos9thpiminply  33948  1smat1  33964  submateqlem1  33967  submateqlem2  33968  xrge0iifcnv  34093  reprlt  34779  reprgt  34781  reprinfz1  34782  erdszelem8  35396  ivthALT  36533  knoppndvlem1  36788  knoppndvlem2  36789  knoppndvlem7  36794  knoppndvlem21  36808  irrdiff  37656  poimirlem1  37956  poimirlem6  37961  poimirlem7  37962  poimirlem9  37964  poimirlem15  37970  poimirlem22  37977  3lexlogpow5ineq1  42507  3lexlogpow5ineq2  42508  3lexlogpow5ineq4  42509  3lexlogpow5ineq3  42510  3lexlogpow2ineq1  42511  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1lem1  42515  dvrelog2b  42519  0nonelalab  42520  dvrelogpow2b  42521  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8d3  42539  aks4d1p8  42540  aks4d1p9  42541  aks6d1c2p2  42572  aks6d1c3  42576  2np3bcnp1  42597  2ap1caineq  42598  sticksstones1  42599  sticksstones2  42600  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones22  42621  aks6d1c6lem4  42626  aks6d1c7lem2  42634  aks5lem8  42654  sn-0ne2  42852  radcnvrat  44759  isosctrlem1ALT  45378  ltdiv23neg  45841  lptre2pt  46086  cncfiooicclem1  46339  cncfioobdlem  46342  ditgeqiooicc  46406  itgioocnicc  46423  iblcncfioo  46424  stirlinglem7  46526  fourierdlem34  46587  fourierdlem42  46595  fourierdlem54  46606  fourierdlem60  46612  fourierdlem73  46625  fourierdlem74  46626  fourierdlem76  46628  fourierdlem81  46633  fourierdlem82  46634  fourierdlem84  46636  fourierdlem93  46645  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierswlem  46676  pimrecltneg  47170  upgrimpthslem2  48396  stgrusgra  48447  eenglngeehlnmlem2  49226