Theorem min1 12996

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

Assertion

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

Proof of Theorem min1

Step	Hyp	Ref	Expression
1		rexr 11094	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 11094	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrmin1 12984	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)
4	1, 2, 3	syl2an 596	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105  ifcif 4471   class class class wbr 5087  ℝcr 10943  ℝ^*cxr 11081   ≤ cle 11083

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 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-pre-lttri 11018  ax-pre-lttrn 11019

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-po 5521  df-so 5522  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 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088

This theorem is referenced by:  ssfzunsnext  13374  reccn2  15378  setsstruct2  16945  ssblex  23653  nlmvscnlem1  23922  nrginvrcnlem  23927  icccmplem2  24058  xlebnum  24200  ipcnlem1  24481  ivthlem2  24688  ioombl1lem4  24797  mbfi1fseqlem5  24956  aalioulem5  25568  aalioulem6  25569  logcnlem3  25871  cxpcn3lem  25972  ftalem5  26298  chtdif  26379  ppidif  26384  chebbnd1lem1  26689  itg2addnc  35887  min1d  43248  mullimc  43394  mullimcf  43401  limcleqr  43422  addlimc  43426  0ellimcdiv  43427  limclner  43429  stoweidlem5  43783  fourierdlem103  43987  fourierdlem104  43988  ioorrnopnlem  44082  hsphoidmvle  44362  hoidmv1lelem1  44367  hoidmv1lelem2  44368  hoidmv1lelem3  44369  smfmullem1  44567