![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifeq12d | Structured version Visualization version GIF version |
Description: Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
Ref | Expression |
---|---|
ifeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
ifeq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
ifeq12d | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifeq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | ifeq1d 4325 | . 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
3 | ifeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | ifeq2d 4326 | . 2 ⊢ (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
5 | 2, 4 | eqtrd 2814 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ifcif 4307 |
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-13 2334 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-nfc 2921 df-rab 3099 df-v 3400 df-un 3797 df-if 4308 |
This theorem is referenced by: ifbieq12d 4334 csbif 4362 oev 7878 dfac12r 9303 xaddpnf1 12369 swrdccat3blem 13871 relexpsucnnr 14172 ruclem1 15364 eucalgval 15701 gsumpropd 17658 gsumpropd2lem 17659 gsumress 17662 mulgfval 17929 mulgpropd 17968 frgpup3lem 18576 subrgmvr 19858 isobs 20463 uvcfval 20527 matsc 20661 scmatscmide 20718 marrepval0 20772 marepvval0 20777 mulmarep1el 20783 madufval 20848 madugsum 20854 minmar1fval 20857 pmat1opsc 20911 pmat1ovscd 20912 mat2pmat1 20944 decpmatid 20982 idpm2idmp 21013 pcoval 23218 pcorevlem 23233 itg2const 23944 ditgeq3 24051 efrlim 25148 lgsval 25478 rpvmasum2 25653 fzto1st 30451 psgnfzto1st 30453 xrhval 30660 itg2addnclem 34088 ftc1anclem5 34116 hdmap1fval 37952 dgrsub2 38668 dirkerval 41239 fourierdlem111 41365 fourierdlem112 41366 fourierdlem113 41367 hsphoif 41721 hsphoival 41724 hoidmvlelem5 41744 hoidifhspval2 41760 hspmbllem2 41772 |
Copyright terms: Public domain | W3C validator |