![]() |
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 8670 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 infcinf 8635 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-ral 3095 df-rex 3096 df-rab 3099 df-uni 4672 df-sup 8636 df-inf 8637 |
This theorem is referenced by: limsupval 14613 lcmval 15711 lcmass 15733 lcmfval 15740 lcmf0val 15741 lcmfpr 15746 odzval 15900 ramval 16116 imasval 16557 imasdsval 16561 gexval 18377 nmofval 22926 nmoval 22927 metdsval 23058 lebnumlem1 23168 lebnumlem3 23170 ovolval 23677 ovolshft 23715 ioorf 23777 mbflimsup 23870 ig1pval 24369 elqaalem1 24511 elqaalem2 24512 elqaalem3 24513 elqaa 24514 omsval 30953 omsfval 30954 ballotlemi 31161 pellfundval 38404 dgraaval 38673 supminfrnmpt 40578 infxrpnf 40580 infxrpnf2 40598 supminfxr 40599 supminfxr2 40604 supminfxrrnmpt 40606 limsupval3 40832 limsupresre 40836 limsupresico 40840 limsuppnfdlem 40841 limsupvaluz 40848 limsupvaluzmpt 40857 liminfval 40899 liminfgval 40902 liminfval5 40905 limsupresxr 40906 liminfresxr 40907 liminfval2 40908 liminfresico 40911 liminf10ex 40914 liminfvalxr 40923 fourierdlem31 41282 ovnval 41682 ovnval2 41686 ovnval2b 41693 ovolval2 41785 ovnovollem3 41799 smfinf 41951 smfinfmpt 41952 prmdvdsfmtnof1 42520 |
Copyright terms: Public domain | W3C validator |