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 8942 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 infcinf 8907 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-in 3945 df-ss 3954 df-uni 4841 df-sup 8908 df-inf 8909 |
This theorem is referenced by: limsupval 14833 lcmval 15938 lcmass 15960 lcmfval 15967 lcmf0val 15968 lcmfpr 15973 odzval 16130 ramval 16346 imasval 16786 imasdsval 16790 gexval 18705 nmofval 23325 nmoval 23326 metdsval 23457 lebnumlem1 23567 lebnumlem3 23569 ovolval 24076 ovolshft 24114 ioorf 24176 mbflimsup 24269 ig1pval 24768 elqaalem1 24910 elqaalem2 24911 elqaalem3 24912 elqaa 24913 omsval 31553 omsfval 31554 ballotlemi 31760 pellfundval 39484 dgraaval 39751 supminfrnmpt 41726 infxrpnf 41728 infxrpnf2 41746 supminfxr 41747 supminfxr2 41752 supminfxrrnmpt 41754 limsupval3 41980 limsupresre 41984 limsupresico 41988 limsuppnfdlem 41989 limsupvaluz 41996 limsupvaluzmpt 42005 liminfval 42047 liminfgval 42050 liminfval5 42053 limsupresxr 42054 liminfresxr 42055 liminfval2 42056 liminfresico 42059 liminf10ex 42062 liminfvalxr 42071 fourierdlem31 42430 ovnval 42830 ovnval2 42834 ovnval2b 42841 ovolval2 42933 ovnovollem3 42947 smfinf 43099 smfinfmpt 43100 prmdvdsfmtnof1 43756 |
Copyright terms: Public domain | W3C validator |