Theorem ltned 11473

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 11472	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
4	3	necomd 3014	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959   class class class wbr 5106  ℝcr 11226   < clt 11370

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-pre-lttri 11301  ax-pre-lttrn 11302

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375

This theorem is used by:  fzodisjsn  13859  fzone1  13946  modsumfzodifsn  14114  seqf1olem1  14211  nprm  16892  4sqlem10  17154  4sqlem17  17168  pgpfaclem2  20328  prmidl0  21664  fvmptnn04ifb  23199  dvferm2lem  26336  lhop2  26365  ftc1lem5  26390  deg1tmle  26466  plyeq0lem  26559  aaliou3lem7  26706  dvloglem  27006  rtprmirr  27118  isosctrlem1  27176  bndatandm  27287  vma1  27523  rplogsumlem2  27842  rpvmasumlem  27844  axlowdimlem13  29562  axlowdimlem16  29565  strlem6  32888  hstrlem6  32896  pmtrto1cl  33730  psgnfzto1stlem  33731  cycpmrn  33774  drngidlhash  34053  krull  34073  esplyfval2  34267  esplyfval3  34274  cos9thpiminply  34490  1smat1  34506  submateqlem1  34509  submateqlem2  34510  xrge0iifcnv  34635  reprlt  35318  reprgt  35320  reprinfz1  35321  erdszelem8  36130  ivthALT  37301  knoppndvlem1  37556  knoppndvlem2  37557  knoppndvlem7  37562  knoppndvlem21  37576  irrdiff  38439  qdiff  38440  poimirlem1  38731  poimirlem6  38736  poimirlem7  38737  poimirlem9  38739  poimirlem15  38745  poimirlem22  38752  3lexlogpow5ineq1  43296  3lexlogpow5ineq2  43297  3lexlogpow5ineq4  43298  3lexlogpow5ineq3  43299  3lexlogpow2ineq1  43300  3lexlogpow2ineq2  43301  3lexlogpow5ineq5  43302  aks4d1lem1  43304  dvrelog2b  43308  0nonelalab  43309  dvrelogpow2b  43310  aks4d1p1p3  43311  aks4d1p1p2  43312  aks4d1p1p4  43313  aks4d1p1p6  43315  aks4d1p1p7  43316  aks4d1p1p5  43317  aks4d1p1  43318  aks4d1p2  43319  aks4d1p3  43320  aks4d1p5  43322  aks4d1p6  43323  aks4d1p7d1  43324  aks4d1p7  43325  aks4d1p8d3  43328  aks4d1p8  43329  aks4d1p9  43330  aks6d1c2p2  43361  aks6d1c3  43365  2np3bcnp1  43386  2ap1caineq  43387  sticksstones1  43388  sticksstones2  43389  sticksstones10  43397  sticksstones12a  43399  sticksstones12  43400  sticksstones22  43410  aks6d1c6lem4  43415  aks6d1c7lem2  43423  aks5lem8  43443  sn-0ne2  43650  radcnvrat  45490  isosctrlem1ALT  46107  ltdiv23neg  46610  lptre2pt  46855  cncfiooicclem1  47108  cncfioobdlem  47111  ditgeqiooicc  47175  itgioocnicc  47192  iblcncfioo  47193  stirlinglem7  47295  fourierdlem34  47356  fourierdlem42  47364  fourierdlem54  47375  fourierdlem60  47381  fourierdlem73  47394  fourierdlem74  47395  fourierdlem76  47397  fourierdlem81  47402  fourierdlem82  47403  fourierdlem84  47405  fourierdlem93  47414  fourierdlem103  47424  fourierdlem104  47425  fourierdlem111  47432  fourierswlem  47445  pimrecltneg  47939  upgrimpthslem2  49211  stgrusgra  49262  eenglngeehlnmlem2  50056