![]() |
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 8624 | . 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 infcinf 8589 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-uni 4629 df-sup 8590 df-inf 8591 |
This theorem is referenced by: limsupval 14546 lcmval 15640 lcmass 15662 lcmfval 15669 lcmf0val 15670 lcmfpr 15675 odzval 15829 ramval 16045 imasval 16486 imasdsval 16490 gexval 18306 nmofval 22846 nmoval 22847 metdsval 22978 lebnumlem1 23088 lebnumlem3 23090 ovolval 23581 ovolshft 23619 ioorf 23681 mbflimsup 23774 ig1pval 24273 elqaalem1 24415 elqaalem2 24416 elqaalem3 24417 elqaa 24418 omsval 30871 omsfval 30872 ballotlemi 31079 pellfundval 38230 dgraaval 38499 supminfrnmpt 40415 infxrpnf 40417 infxrpnf2 40436 supminfxr 40437 supminfxr2 40442 supminfxrrnmpt 40444 limsupval3 40668 limsupresre 40672 limsupresico 40676 limsuppnfdlem 40677 limsupvaluz 40684 limsupvaluzmpt 40693 liminfval 40735 liminfgval 40738 liminfval5 40741 limsupresxr 40742 liminfresxr 40743 liminfval2 40744 liminfresico 40747 liminf10ex 40750 liminfvalxr 40759 fourierdlem31 41098 ovnval 41501 ovnval2 41505 ovnval2b 41512 ovolval2 41604 ovnovollem3 41618 smfinf 41770 smfinfmpt 41771 prmdvdsfmtnof1 42281 |
Copyright terms: Public domain | W3C validator |