Theorem lttrd 11215

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 11130	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1370	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 696	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105   class class class wbr 5086  ℝcr 10949   < clt 11088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-resscn 11007  ax-pre-lttrn 11025

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-mpt 5170  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-er 8547  df-en 8783  df-dom 8784  df-sdom 8785  df-pnf 11090  df-mnf 11091  df-ltxr 11093

This theorem is referenced by:  nnne0  12086  expgt1  13900  ltexp2a  13963  expcan  13966  ltexp2  13967  leexp2  13968  expnlbnd2  14028  expmulnbnd  14029  reccn2  15382  efgt1  15901  tanhlt1  15945  ruclem2  16017  isprm7  16487  pythagtriplem13  16602  fldivp1  16672  4sqlem12  16731  sylow1lem1  19276  telgsums  19666  chfacffsupp  22085  chfacfscmul0  22087  chfacfpmmul0  22091  nrginvrcnlem  23935  iccntr  24064  icccmplem2  24066  opnreen  24074  pjthlem1  24681  pmltpclem2  24693  ovollb2lem  24732  opnmbllem  24845  volivth  24851  lhop1lem  25257  dvcnvrelem1  25261  dvcvx  25264  ftc1lem4  25283  aaliou3lem7  25589  ulmdvlem1  25639  reeff1olem  25685  pilem2  25691  pilem3  25692  tangtx  25742  tanord1  25773  tanord  25774  rplogcl  25839  logimul  25849  logcnlem3  25879  efopnlem1  25891  cxplt  25929  cxple  25930  cxpcn3lem  25980  asinsin  26122  atanlogaddlem  26143  atanlogsublem  26145  cxp2limlem  26205  cxp2lim  26206  zetacvg  26244  lgamucov  26267  lgamcvg2  26284  ftalem1  26302  mersenne  26455  bposlem2  26513  bposlem6  26517  bposlem9  26520  lgsqrlem2  26575  lgsquadlem2  26609  chebbnd1lem2  26698  chebbnd1lem3  26699  chebbnd1  26700  chtppilimlem1  26701  chto1ub  26704  mulog2sumlem2  26763  chpdifbndlem1  26781  selberg3lem1  26785  pntrlog2bndlem2  26806  pntrlog2bndlem4  26808  pntpbnd1a  26813  pntpbnd1  26814  pntpbnd2  26815  pntibndlem1  26817  pntibndlem2  26819  pntibndlem3  26820  pntibnd  26821  pntlemb  26825  pntlemr  26830  pntlemf  26833  pnt  26842  ostth2lem1  26846  ostth2lem3  26863  ostth2lem4  26864  wwlksext2clwwlk  28553  frgrogt3nreg  28893  friendshipgt3  28894  pjhthlem1  29885  psgnfzto1stlem  31498  1smat1  31890  sqsscirc1  31994  xrge0iifiso  32021  sgnsub  32647  signslema  32677  chtvalz  32745  hgt750lemd  32764  knoppndvlem12  34773  knoppndvlem14  34775  knoppndvlem15  34776  knoppndvlem17  34778  knoppndvlem20  34781  poimirlem6  35860  poimirlem7  35861  poimirlem8  35862  poimirlem15  35869  poimirlem20  35874  poimirlem28  35882  opnmbllem0  35890  itg2gt0cn  35909  ftc1cnnclem  35925  ftc1anc  35935  cntotbnd  36031  3lexlogpow5ineq3  40291  3lexlogpow2ineq2  40293  3lexlogpow5ineq5  40294  aks4d1lem1  40296  0nonelalab  40301  aks4d1p1p3  40303  aks4d1p1p2  40304  aks4d1p1p4  40305  aks4d1p1p6  40307  aks4d1p1p7  40308  aks4d1p1p5  40309  aks4d1p1  40310  aks4d1p2  40311  aks4d1p3  40312  aks4d1p6  40315  aks4d1p7d1  40316  aks4d1p7  40317  aks4d1p8d3  40320  aks4d1p8  40321  2ap1caineq  40330  sticksstones1  40331  flt4lem7  40717  fltnlta  40721  pellexlem5  40876  pellfundex  40929  pellfundrp  40931  rmspecfund  40952  monotuz  40985  jm3.1lem2  41062  jm3.1lem3  41063  imo72b2  42022  prmunb2  42168  neglt  43077  ltadd12dd  43136  infleinflem2  43164  sqrlearg  43346  lptre2pt  43436  0ellimcdiv  43445  limsup10exlem  43568  ioodvbdlimc1lem1  43727  iblspltprt  43769  itgspltprt  43775  stoweidlem7  43803  stoweidlem11  43807  stoweidlem13  43809  stoweidlem14  43810  stoweidlem26  43822  stoweidlem42  43838  stoweidlem52  43848  stoweidlem59  43855  stoweidlem60  43856  stoweidlem62  43858  wallispilem4  43864  wallispi  43866  stirlinglem1  43870  stirlinglem3  43872  stirlinglem6  43875  stirlinglem7  43876  stirlinglem10  43879  stirlinglem11  43880  dirkercncflem1  43899  dirkercncflem2  43900  fourierdlem10  43913  fourierdlem11  43914  fourierdlem12  43915  fourierdlem42  43945  fourierdlem47  43949  fourierdlem50  43952  fourierdlem51  43953  fourierdlem73  43975  fourierdlem79  43981  fourierdlem83  43985  fourierdlem103  44005  fourierdlem104  44006  sqwvfoura  44024  sqwvfourb  44025  fouriersw  44027  hoidmvlelem1  44389  hoiqssbllem2  44417  hspmbllem1  44420  pimrecltpos  44502  pimrecltneg  44518  smfaddlem1  44557  smflimlem3  44567  smflimlem4  44568  smfmullem1  44585  fpprel2  45463  eenglngeehlnmlem2  46354