Theorem ltned 10854

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2934   class class class wbr 5030  ℝcr 10614   < clt 10753

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-resscn 10672  ax-pre-lttri 10689  ax-pre-lttrn 10690

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-po 5442  df-so 5443  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-er 8320  df-en 8556  df-dom 8557  df-sdom 8558  df-pnf 10755  df-mnf 10756  df-ltxr 10758

This theorem is referenced by:  fzodisjsn  13166  modsumfzodifsn  13403  seqf1olem1  13501  nprm  16129  4sqlem10  16383  4sqlem17  16397  pgpfaclem2  19323  fvmptnn04ifb  21602  dvferm2lem  24738  lhop2  24767  ftc1lem5  24792  deg1tmle  24870  plyeq0lem  24959  aaliou3lem7  25097  dvloglem  25391  isosctrlem1  25556  bndatandm  25667  vma1  25903  rplogsumlem2  26221  rpvmasumlem  26223  axlowdimlem13  26900  axlowdimlem16  26903  strlem6  30191  hstrlem6  30199  fzone1  30696  pmtrto1cl  30943  psgnfzto1stlem  30944  cycpmrn  30987  prmidl0  31198  krull  31215  1smat1  31326  submateqlem1  31329  submateqlem2  31330  madjusmdetlem2  31350  xrge0iifcnv  31455  reprlt  32169  reprgt  32171  reprinfz1  32172  erdszelem8  32731  ivthALT  34167  knoppndvlem1  34335  knoppndvlem2  34336  knoppndvlem7  34341  knoppndvlem21  34355  irrdiff  35137  poimirlem1  35421  poimirlem6  35426  poimirlem7  35427  poimirlem9  35429  poimirlem15  35435  poimirlem22  35442  3lexlogpow5ineq1  39702  3lexlogpow5ineq2  39703  3lexlogpow5ineq4  39704  3lexlogpow5ineq3  39705  3lexlogpow2ineq1  39706  3lexlogpow2ineq2  39707  3lexlogpow5ineq5  39708  dvrelog2b  39713  0nonelalab  39714  dvrelogpow2b  39715  aks4d1p1p3  39716  aks4d1p1p2  39717  aks4d1p1p4  39718  aks4d1p1p6  39720  aks4d1p1p7  39721  aks4d1p1p5  39722  aks4d1p1  39723  2np3bcnp1  39726  2ap1caineq  39727  sticksstones1  39728  sticksstones2  39729  metakunt6  39741  metakunt7  39742  metakunt11  39746  metakunt12  39747  metakunt27  39762  metakunt28  39763  metakunt29  39764  metakunt30  39765  rtprmirr  39944  sn-0ne2  39986  radcnvrat  41490  isosctrlem1ALT  42112  ltdiv23neg  42492  lptre2pt  42743  cncfiooicclem1  42996  cncfioobdlem  42999  ditgeqiooicc  43063  itgioocnicc  43080  iblcncfioo  43081  stirlinglem7  43183  fourierdlem34  43244  fourierdlem42  43252  fourierdlem54  43263  fourierdlem60  43269  fourierdlem73  43282  fourierdlem74  43283  fourierdlem76  43285  fourierdlem81  43290  fourierdlem82  43291  fourierdlem84  43293  fourierdlem93  43302  fourierdlem103  43312  fourierdlem104  43313  fourierdlem111  43320  fourierswlem  43333  pimrecltneg  43819  eenglngeehlnmlem2  45638