Theorem leidd 8437

Description: 'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
leidd.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
leidd	|- ( ph -> A <_ A )

Proof of Theorem leidd

Step	Hyp	Ref	Expression
1		leidd.1	. 2 |- ( ph -> A e. RR )
2		leid 8007	. 2 |- ( A e. RR -> A <_ A )
3	1, 2	syl 14	1 |- ( ph -> A <_ A )

Syntax hints:   -> wi 4   e. wcel 2142   class class class wbr 3990   RRcr 7777   <_ cle 7959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-setind 4522  ax-cnex 7869  ax-resscn 7870  ax-pre-ltirr 7890

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-fal 1355  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-nel 2437  df-ral 2454  df-rex 2455  df-rab 2458  df-v 2733  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-opab 4052  df-xp 4618  df-cnv 4620  df-pnf 7960  df-mnf 7961  df-xr 7962  df-ltxr 7963  df-le 7964

This theorem is referenced by:  zextle  9307  uzind  9327  uzid  9505  z2ge  9787  nn0fz0  10079  fvinim0ffz  10201  flid  10244  modqabs2  10318  monoord  10436  leexp2r  10534  facwordi  10678  faclbnd6  10682  sqrtgt0  11002  abs00ap  11030  isumlessdc  11463  cvgratnnlemnexp  11491  cvgratnnlemmn  11492  eirraplem  11743  nn0seqcvgd  11999  pcidlem  12280  pc2dvds  12287  pcprmpw2  12290  pcmpt  12299  trilpolemclim  14153  trilpolemisumle  14155  trilpolemeq1  14157