Theorem min1 11512

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

Assertion

Ref	Expression
min1	|- ( ( A e. RR /\ B e. RR ) -> if ( A <_ B , A , B ) <_ A )

Proof of Theorem min1

Step	Hyp	Ref	Expression
1		rexr 9712	. 2 |- ( A e. RR -> A e. RR* )
2		rexr 9712	. 2 |- ( B e. RR -> B e. RR* )
3		xrmin1 11501	. 2 |- ( ( A e. RR* /\ B e. RR* ) -> if ( A <_ B , A , B ) <_ A )
4	1, 2, 3	syl2an 484	1 |- ( ( A e. RR /\ B e. RR ) -> if ( A <_ B , A , B ) <_ A )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1898   ifcif 3893   class class class wbr 4416   RRcr 9564   RR*cxr 9700   <_ cle 9702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-pre-lttri 9639  ax-pre-lttrn 9640

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707

This theorem is referenced by:  reccn2  13709  ssblex  21492  nlmvscnlem1  21738  nrginvrcnlem  21742  icccmplem2  21890  xlebnum  22045  ipcnlem1  22265  ivthlem2  22452  ioombl1lem4  22563  mbfi1fseqlem5  22726  aalioulem5  23341  aalioulem6  23342  logcnlem3  23638  cxpcn3lem  23736  ftalem5  24050  ftalem5OLD  24052  chtdif  24134  ppidif  24139  chebbnd1lem1  24356  itg2addnc  32041  mullimc  37734  mullimcf  37741  limcleqr  37763  addlimc  37767  0ellimcdiv  37768  limclner  37770  stoweidlem5  37903  fourierdlem103  38111  fourierdlem104  38112  hsphoidmvle  38446  hoidmv1lelem1  38451  hoidmv1lelem2  38452  hoidmv1lelem3  38453