Theorem min2 13179

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 11214	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 11214	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrmin2 13167	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
4	1, 2, 3	syl2an 604	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2132  ifcif 4470   class class class wbr 5090  ℝcr 11058  ℝ^*cxr 11201   ≤ cle 11203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-cnex 11115  ax-resscn 11116  ax-pre-lttri 11133  ax-pre-lttrn 11134

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-xr 11206  df-ltxr 11207  df-le 11208

This theorem is referenced by:  ssfzunsnext  13560  reccn2  15596  ssblex  24457  nlmvscnlem1  24715  nrginvrcnlem  24720  icccmplem2  24853  xlebnum  24996  ipcnlem1  25276  ivthlem2  25483  ovolicc2lem5  25552  ioombl1lem1  25589  mbfi1fseqlem4  25749  mbfi1fseqlem5  25750  aalioulem5  26366  aalioulem6  26367  cxpcn3lem  26778  ftalem5  27107  chtdif  27188  ppidif  27193  chebbnd1lem1  27499  itg2addnc  38111  min2d  45985  mullimc  46130  mullimcf  46137  limcleqr  46156  addlimc  46160  0ellimcdiv  46161  limclner  46163  stoweidlem5  46517  fourierdlem104  46722  ioorrnopnlem  46816  hoidmv1lelem2  47104  smfmullem1  47303