Theorem lttrd 11372

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   class class class wbr 5110  ℝcr 11100   < clt 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-pre-lttrn 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  mulgt1  12077  nnne0  12271  neglt  13037  expgt1  14138  ltexp2a  14204  expcan  14207  ltexp2  14208  leexp2  14209  expnlbnd2  14272  expmulnbnd  14273  sgnsub  15145  reccn2  15650  efgt1  16173  tanhlt1  16217  ruclem2  16289  isprm7  16768  pythagtriplem13  16888  fldivp1  16958  4sqlem12  17017  chnub  18679  chnccat  18683  sylow1lem1  19669  telgsums  20064  chfacffsupp  22994  chfacfscmul0  22996  chfacfpmmul0  23000  nrginvrcnlem  24829  iccntr  24960  icccmplem2  24962  opnreen  24970  pjthlem1  25577  pmltpclem2  25589  ovollb2lem  25628  opnmbllem  25741  volivth  25747  lhop1lem  26153  dvcnvrelem1  26157  dvcvx  26160  ftc1lem4  26179  aaliou3lem7  26493  ulmdvlem1  26544  reeff1olem  26590  pilem2  26596  pilem3  26597  tangtx  26651  tanord1  26683  tanord  26684  rplogcl  26750  logimul  26760  logcnlem3  26790  efopnlem1  26802  cxplt  26840  cxple  26841  cxpcn3lem  26893  asinsin  27038  atanlogaddlem  27059  atanlogsublem  27061  cxp2limlem  27121  cxp2lim  27122  zetacvg  27160  lgamucov  27183  lgamcvg2  27200  ftalem1  27218  mersenne  27372  bposlem2  27430  bposlem6  27434  bposlem9  27437  lgsqrlem2  27492  lgsquadlem2  27526  chebbnd1lem2  27615  chebbnd1lem3  27616  chebbnd1  27617  chtppilimlem1  27618  chto1ub  27621  mulog2sumlem2  27680  chpdifbndlem1  27698  selberg3lem1  27702  pntrlog2bndlem2  27723  pntrlog2bndlem4  27725  pntpbnd1a  27730  pntpbnd1  27731  pntpbnd2  27732  pntibndlem1  27734  pntibndlem2  27736  pntibndlem3  27737  pntibnd  27738  pntlemb  27742  pntlemr  27747  pntlemf  27750  pnt  27759  ostth2lem1  27763  ostth2lem3  27780  ostth2lem4  27781  wwlksext2clwwlk  30389  frgrogt3nreg  30729  friendshipgt3  30730  pjhthlem1  31724  psgnfzto1stlem  33401  1smat1  34175  sqsscirc1  34279  xrge0iifiso  34306  signslema  34930  chtvalz  34997  hgt750lemd  35016  knoppndvlem12  37093  knoppndvlem14  37095  knoppndvlem15  37096  knoppndvlem17  37098  knoppndvlem20  37101  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem15  38267  poimirlem20  38272  poimirlem28  38280  opnmbllem0  38288  itg2gt0cn  38307  ftc1cnnclem  38323  ftc1anc  38333  cntotbnd  38428  3lexlogpow5ineq3  42805  3lexlogpow2ineq2  42807  3lexlogpow5ineq5  42808  aks4d1lem1  42810  0nonelalab  42815  aks4d1p1p3  42817  aks4d1p1p2  42818  aks4d1p1p4  42819  aks4d1p1p6  42821  aks4d1p1p7  42822  aks4d1p1p5  42823  aks4d1p1  42824  aks4d1p2  42825  aks4d1p3  42826  aks4d1p6  42829  aks4d1p7d1  42830  aks4d1p7  42831  aks4d1p8d3  42834  aks4d1p8  42835  2ap1caineq  42893  sticksstones1  42894  sn-addlt0d  43213  sn-addgt0d  43214  sn-mulgt1d  43234  fimgmcyc  43285  flt4lem7  43374  fltnlta  43378  pellexlem5  43543  pellfundex  43596  pellfundrp  43598  rmspecfund  43619  monotuz  43651  jm3.1lem2  43728  jm3.1lem3  43729  imo72b2  44881  prmunb2  45004  ltadd12dd  46042  infleinflem2  46069  sqrlearg  46252  lptre2pt  46337  0ellimcdiv  46346  limsup10exlem  46469  ioodvbdlimc1lem1  46628  iblspltprt  46670  itgspltprt  46676  stoweidlem7  46704  stoweidlem11  46708  stoweidlem13  46710  stoweidlem14  46711  stoweidlem26  46723  stoweidlem42  46739  stoweidlem52  46749  stoweidlem59  46756  stoweidlem60  46757  stoweidlem62  46759  wallispilem4  46765  wallispi  46767  stirlinglem1  46771  stirlinglem3  46773  stirlinglem6  46776  stirlinglem7  46777  stirlinglem10  46780  stirlinglem11  46781  dirkercncflem1  46800  dirkercncflem2  46801  fourierdlem10  46814  fourierdlem11  46815  fourierdlem12  46816  fourierdlem42  46846  fourierdlem47  46850  fourierdlem50  46853  fourierdlem51  46854  fourierdlem73  46876  fourierdlem79  46882  fourierdlem83  46886  fourierdlem103  46906  fourierdlem104  46907  sqwvfoura  46925  sqwvfourb  46926  fouriersw  46928  hoidmvlelem1  47292  hoiqssbllem2  47320  hspmbllem1  47323  pimrecltpos  47405  pimrecltneg  47421  smfaddlem1  47460  smflimlem3  47470  smflimlem4  47471  smfmullem1  47488  ormkglobd  47574  chnsubseq  47579  difmodm1lt  48085  2timesltsqm1  48099  fpprel2  48489  gpgedgvtx0  48809  gpgedgvtx1  48810  eenglngeehlnmlem2  49501