Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > infeq1d | Structured version Visualization version GIF version |
Description: Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
Ref | Expression |
---|---|
infeq1d.1 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
infeq1d | ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | infeq1d.1 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
2 | infeq1 8934 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 infcinf 8899 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-ral 3143 df-rex 3144 df-rab 3147 df-uni 4833 df-sup 8900 df-inf 8901 |
This theorem is referenced by: limsupval 14825 lcmval 15930 lcmass 15952 lcmfval 15959 lcmf0val 15960 lcmfpr 15965 odzval 16122 ramval 16338 imasval 16778 imasdsval 16782 gexval 18697 nmofval 23317 nmoval 23318 metdsval 23449 lebnumlem1 23559 lebnumlem3 23561 ovolval 24068 ovolshft 24106 ioorf 24168 mbflimsup 24261 ig1pval 24760 elqaalem1 24902 elqaalem2 24903 elqaalem3 24904 elqaa 24905 omsval 31546 omsfval 31547 ballotlemi 31753 pellfundval 39470 dgraaval 39737 supminfrnmpt 41711 infxrpnf 41713 infxrpnf2 41731 supminfxr 41732 supminfxr2 41737 supminfxrrnmpt 41739 limsupval3 41965 limsupresre 41969 limsupresico 41973 limsuppnfdlem 41974 limsupvaluz 41981 limsupvaluzmpt 41990 liminfval 42032 liminfgval 42035 liminfval5 42038 limsupresxr 42039 liminfresxr 42040 liminfval2 42041 liminfresico 42044 liminf10ex 42047 liminfvalxr 42056 fourierdlem31 42416 ovnval 42816 ovnval2 42820 ovnval2b 42827 ovolval2 42919 ovnovollem3 42933 smfinf 43085 smfinfmpt 43086 prmdvdsfmtnof1 43742 |
Copyright terms: Public domain | W3C validator |