![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ifeq1d | GIF version |
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Ref | Expression |
---|---|
ifeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
ifeq1d | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | ifeq1 3504 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1332 ifcif 3501 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-ext 2136 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1740 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-rab 2441 df-v 2711 df-un 3102 df-if 3502 |
This theorem is referenced by: ifeq12d 3520 ifbieq1d 3523 ifeq1dadc 3531 iseqf1olemjpcl 10372 iseqf1olemqpcl 10373 iseqf1olemfvp 10374 seq3f1olemqsum 10377 seq3f1olemp 10379 summodc 11257 fsum3 11261 fsum3ser 11271 isumlessdc 11370 prodeq2w 11430 prodmodc 11452 fprodseq 11457 prodssdc 11463 |
Copyright terms: Public domain | W3C validator |