Theorem ltned 11310

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925   class class class wbr 5107  ℝcr 11067   < clt 11208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-pre-lttri 11142  ax-pre-lttrn 11143

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213

This theorem is referenced by:  fzodisjsn  13658  modsumfzodifsn  13909  seqf1olem1  14006  nprm  16658  4sqlem10  16918  4sqlem17  16932  pgpfaclem2  20014  fvmptnn04ifb  22738  dvferm2lem  25890  lhop2  25920  ftc1lem5  25947  deg1tmle  26023  plyeq0lem  26115  aaliou3lem7  26257  dvloglem  26557  rtprmirr  26670  isosctrlem1  26728  bndatandm  26839  vma1  27076  rplogsumlem2  27396  rpvmasumlem  27398  axlowdimlem13  28881  axlowdimlem16  28884  strlem6  32185  hstrlem6  32193  fzone1  32723  pmtrto1cl  33056  psgnfzto1stlem  33057  cycpmrn  33100  drngidlhash  33405  prmidl0  33421  krull  33450  cos9thpiminply  33778  1smat1  33794  submateqlem1  33797  submateqlem2  33798  xrge0iifcnv  33923  reprlt  34610  reprgt  34612  reprinfz1  34613  erdszelem8  35185  ivthALT  36323  knoppndvlem1  36500  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem21  36520  irrdiff  37314  poimirlem1  37615  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem15  37629  poimirlem22  37636  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  dvrelog2b  42054  0nonelalab  42055  dvrelogpow2b  42056  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8d3  42074  aks4d1p8  42075  aks4d1p9  42076  aks6d1c2p2  42107  aks6d1c3  42111  2np3bcnp1  42132  2ap1caineq  42133  sticksstones1  42134  sticksstones2  42135  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem4  42161  aks6d1c7lem2  42169  aks5lem8  42189  sn-0ne2  42394  radcnvrat  44303  isosctrlem1ALT  44923  ltdiv23neg  45390  lptre2pt  45638  cncfiooicclem1  45891  cncfioobdlem  45894  ditgeqiooicc  45958  itgioocnicc  45975  iblcncfioo  45976  stirlinglem7  46078  fourierdlem34  46139  fourierdlem42  46147  fourierdlem54  46158  fourierdlem60  46164  fourierdlem73  46177  fourierdlem74  46178  fourierdlem76  46180  fourierdlem81  46185  fourierdlem82  46186  fourierdlem84  46188  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierswlem  46228  pimrecltneg  46722  upgrimpthslem2  47908  stgrusgra  47958  eenglngeehlnmlem2  48727