Theorem lttrd 11335

Description: Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.)

Hypotheses

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

Assertion

Ref	Expression
lttrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem lttrd

Step	Hyp	Ref	Expression
1		lttrd.4	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		lttrd.5	. 2 ⊢ (𝜑 → 𝐵 < 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		lttr 11250	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 699	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   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-lttrn 11143

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  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-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:  mulgt1  12044  nnne0  12220  neglt  12971  expgt1  14065  ltexp2a  14131  expcan  14134  ltexp2  14135  leexp2  14136  expnlbnd2  14199  expmulnbnd  14200  reccn2  15563  efgt1  16084  tanhlt1  16128  ruclem2  16200  isprm7  16678  pythagtriplem13  16798  fldivp1  16868  4sqlem12  16927  sylow1lem1  19528  telgsums  19923  chfacffsupp  22743  chfacfscmul0  22745  chfacfpmmul0  22749  nrginvrcnlem  24579  iccntr  24710  icccmplem2  24712  opnreen  24720  pjthlem1  25337  pmltpclem2  25350  ovollb2lem  25389  opnmbllem  25502  volivth  25508  lhop1lem  25918  dvcnvrelem1  25922  dvcvx  25925  ftc1lem4  25946  aaliou3lem7  26257  ulmdvlem1  26309  reeff1olem  26356  pilem2  26362  pilem3  26363  tangtx  26414  tanord1  26446  tanord  26447  rplogcl  26513  logimul  26523  logcnlem3  26553  efopnlem1  26565  cxplt  26603  cxple  26604  cxpcn3lem  26657  asinsin  26802  atanlogaddlem  26823  atanlogsublem  26825  cxp2limlem  26886  cxp2lim  26887  zetacvg  26925  lgamucov  26948  lgamcvg2  26965  ftalem1  26983  mersenne  27138  bposlem2  27196  bposlem6  27200  bposlem9  27203  lgsqrlem2  27258  lgsquadlem2  27292  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chto1ub  27387  mulog2sumlem2  27446  chpdifbndlem1  27464  selberg3lem1  27468  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem1  27500  pntibndlem2  27502  pntibndlem3  27503  pntibnd  27504  pntlemb  27508  pntlemr  27513  pntlemf  27516  pnt  27525  ostth2lem1  27529  ostth2lem3  27546  ostth2lem4  27547  wwlksext2clwwlk  29986  frgrogt3nreg  30326  friendshipgt3  30327  pjhthlem1  31320  sgnsub  32762  chnub  32938  psgnfzto1stlem  33057  1smat1  33794  sqsscirc1  33898  xrge0iifiso  33925  signslema  34553  chtvalz  34620  hgt750lemd  34639  knoppndvlem12  36511  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem20  36519  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem15  37629  poimirlem20  37634  poimirlem28  37642  opnmbllem0  37650  itg2gt0cn  37669  ftc1cnnclem  37685  ftc1anc  37695  cntotbnd  37790  3lexlogpow5ineq3  42045  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  0nonelalab  42055  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8d3  42074  aks4d1p8  42075  2ap1caineq  42133  sticksstones1  42134  sn-addlt0d  42446  sn-addgt0d  42447  sn-mulgt1d  42467  fimgmcyc  42522  flt4lem7  42647  fltnlta  42651  pellexlem5  42821  pellfundex  42874  pellfundrp  42876  rmspecfund  42897  monotuz  42930  jm3.1lem2  43007  jm3.1lem3  43008  imo72b2  44161  prmunb2  44300  ltadd12dd  45339  infleinflem2  45367  sqrlearg  45551  lptre2pt  45638  0ellimcdiv  45647  limsup10exlem  45770  ioodvbdlimc1lem1  45929  iblspltprt  45971  itgspltprt  45977  stoweidlem7  46005  stoweidlem11  46009  stoweidlem13  46011  stoweidlem14  46012  stoweidlem26  46024  stoweidlem42  46040  stoweidlem52  46050  stoweidlem59  46057  stoweidlem60  46058  stoweidlem62  46060  wallispilem4  46066  wallispi  46068  stirlinglem1  46072  stirlinglem3  46074  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  dirkercncflem1  46101  dirkercncflem2  46102  fourierdlem10  46115  fourierdlem11  46116  fourierdlem12  46117  fourierdlem42  46147  fourierdlem47  46151  fourierdlem50  46154  fourierdlem51  46155  fourierdlem73  46177  fourierdlem79  46183  fourierdlem83  46187  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  hoidmvlelem1  46593  hoiqssbllem2  46621  hspmbllem1  46624  pimrecltpos  46706  pimrecltneg  46722  smfaddlem1  46761  smflimlem3  46771  smflimlem4  46772  smfmullem1  46789  ormkglobd  46873  difmodm1lt  47360  fpprel2  47742  gpgedgvtx0  48052  gpgedgvtx1  48053  eenglngeehlnmlem2  48727