Theorem letrd 8216

Description: Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
letrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
letrd.4	⊢ (𝜑 → 𝐴 ≤ 𝐵)
letrd.5	⊢ (𝜑 → 𝐵 ≤ 𝐶)

Assertion

Ref	Expression
letrd	⊢ (𝜑 → 𝐴 ≤ 𝐶)

Proof of Theorem letrd

Step	Hyp	Ref	Expression
1		letrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		letrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		letr 8175	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
7	3, 4, 5, 6	syl3anc 1250	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
8	1, 2, 7	mp2and 433	1 ⊢ (𝜑 → 𝐴 ≤ 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177   class class class wbr 4051  ℝcr 7944   ≤ cle 8128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261  ax-un 4488  ax-setind 4593  ax-cnex 8036  ax-resscn 8037  ax-pre-ltwlin 8058

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-xp 4689  df-cnv 4691  df-pnf 8129  df-mnf 8130  df-xr 8131  df-ltxr 8132  df-le 8133

This theorem is referenced by:  nn0negleid  9461  eluzuzle  9676  infregelbex  9739  fzdisj  10194  difelfzle  10276  infssuzex  10398  suprzubdc  10401  flqwordi  10453  btwnzge0  10465  fldiv4lem1div2uz2  10471  flqleceil  10484  modqltm1p1mod  10543  seq3split  10655  iseqf1olemqcl  10666  iseqf1olemnab  10668  iseqf1olemab  10669  seq3f1olemqsumkj  10678  seq3f1olemqsumk  10679  seq3f1olemqsum  10680  seqf1oglem1  10686  seqfeq4g  10698  bernneq  10827  bernneq3  10829  zzlesq  10875  nn0opthlem2d  10888  faclbnd  10908  facubnd  10912  seq3coll  11009  resqrexlemover  11396  resqrexlemdecn  11398  resqrexlemcalc3  11402  absle  11475  releabs  11482  maxleastb  11600  nn0maxcl  11611  climsqz  11721  climsqz2  11722  fsum3cvg3  11782  expcnvap0  11888  geolim2  11898  cvgratnnlemabsle  11913  cvgratnnlemfm  11915  cvgratnnlemrate  11916  cvgratz  11918  mertenslem2  11922  eftlub  12076  cos12dec  12154  divalglemnqt  12306  bitsfzo  12341  ncoprmgcdne1b  12486  prmdc  12527  isprm5lem  12538  eulerthlemrprm  12626  eulerthlema  12627  pcmpt2  12742  pcfac  12748  4sqexercise2  12797  4sqlemsdc  12798  4sqlem11  12799  ennnfoneleminc  12857  ennnfonelemkh  12858  nninfdclemlt  12897  strleund  13010  strext  13012  gsumfzfsumlemm  14424  psrbaglesuppg  14509  suplociccex  15172  ivthinclemlopn  15183  ivthinclemuopn  15185  dveflem  15273  cosordlem  15396  rpabscxpbnd  15487  lgsdirprm  15586  lgsquadlem1  15629  2lgslem1c  15642  2sqlem8  15675