Theorem min2 12581

Description: The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.)

Assertion

Ref	Expression
min2	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)

Proof of Theorem min2

Step	Hyp	Ref	Expression
1		rexr 10684	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 10684	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrmin2 12569	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
4	1, 2, 3	syl2an 597	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  ifcif 4464   class class class wbr 5063  ℝcr 10533  ℝ^*cxr 10671   ≤ cle 10673

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5327  ax-un 7458  ax-cnex 10590  ax-resscn 10591  ax-pre-lttri 10608  ax-pre-lttrn 10609

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-nel 3123  df-ral 3142  df-rex 3143  df-rab 3146  df-v 3495  df-sbc 3771  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4465  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4836  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5457  df-po 5471  df-so 5472  df-xp 5558  df-rel 5559  df-cnv 5560  df-co 5561  df-dm 5562  df-rn 5563  df-res 5564  df-ima 5565  df-iota 6311  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-er 8286  df-en 8507  df-dom 8508  df-sdom 8509  df-pnf 10674  df-mnf 10675  df-xr 10676  df-ltxr 10677  df-le 10678

This theorem is referenced by:  ssfzunsnext  12950  reccn2  14949  ssblex  23034  nlmvscnlem1  23291  nrginvrcnlem  23296  icccmplem2  23427  xlebnum  23565  ipcnlem1  23844  ivthlem2  24049  ovolicc2lem5  24118  ioombl1lem1  24155  mbfi1fseqlem4  24315  mbfi1fseqlem5  24316  aalioulem5  24923  aalioulem6  24924  cxpcn3lem  25326  ftalem5  25652  chtdif  25733  ppidif  25738  chebbnd1lem1  26043  itg2addnc  34984  min2d  41823  mullimc  41971  mullimcf  41978  limcleqr  41999  addlimc  42003  0ellimcdiv  42004  limclner  42006  stoweidlem5  42364  fourierdlem104  42569  ioorrnopnlem  42663  hoidmv1lelem2  42948  smfmullem1  43140