ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lelttr GIF version

Theorem lelttr 7106
Description: Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.)
Assertion
Ref Expression
lelttr ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Proof of Theorem lelttr
StepHypRef Expression
1 simprl 483 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → 𝐴𝐵)
2 simpl1 907 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → 𝐴 ∈ ℝ)
3 simpl2 908 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → 𝐵 ∈ ℝ)
4 lenlt 7094 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
52, 3, 4syl2anc 391 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
61, 5mpbid 135 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → ¬ 𝐵 < 𝐴)
76pm2.21d 549 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → (𝐵 < 𝐴𝐴 < 𝐶))
8 idd 21 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → (𝐴 < 𝐶𝐴 < 𝐶))
9 simprr 484 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → 𝐵 < 𝐶)
10 simpl3 909 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → 𝐶 ∈ ℝ)
11 axltwlin 7087 . . . . 5 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐶 → (𝐵 < 𝐴𝐴 < 𝐶)))
123, 10, 2, 11syl3anc 1135 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → (𝐵 < 𝐶 → (𝐵 < 𝐴𝐴 < 𝐶)))
139, 12mpd 13 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → (𝐵 < 𝐴𝐴 < 𝐶))
147, 8, 13mpjaod 638 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴𝐵𝐵 < 𝐶)) → 𝐴 < 𝐶)
1514ex 108 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 97  wb 98  wo 629  w3a 885  wcel 1393   class class class wbr 3764  cr 6888   < clt 7060  cle 7061
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-cnex 6975  ax-resscn 6976  ax-pre-ltwlin 6997
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-nel 2207  df-ral 2311  df-rex 2312  df-rab 2315  df-v 2559  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-xp 4351  df-cnv 4353  df-pnf 7062  df-mnf 7063  df-xr 7064  df-ltxr 7065  df-le 7066
This theorem is referenced by:  lelttri  7123  lelttrd  7139  letrp1  7814  ltmul12a  7826  bndndx  8180  uzind  8349  fnn0ind  8354  elfzo0z  9040  fzofzim  9044  elfzodifsumelfzo  9057  flqge  9124  expnlbnd2  9374  caubnd2  9713  mulcn2  9833  cn1lem  9834  climsqz  9855  climsqz2  9856  climcvg1nlem  9868  algcvgblem  9888
  Copyright terms: Public domain W3C validator