| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > ifbid | GIF version | ||
| Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.) |
| Ref | Expression |
|---|---|
| ifbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| ifbid | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ifbid.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | ifbi 3590 | . 2 ⊢ ((𝜓 ↔ 𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) | |
| 3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ wb 105 = wceq 1372 ifcif 3570 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-11 1528 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-if 3571 |
| This theorem is referenced by: ifbieq1d 3592 ifbieq2d 3594 ifbieq12d 3596 ifandc 3609 ifordc 3610 pw2f1odclem 6930 nnnninf 7227 nnnninf2 7228 nnnninfeq 7229 nninfisollemne 7232 nninfisol 7234 fodjum 7247 fodju0 7248 fodjuomni 7250 fodjumkv 7261 nninfwlporlemd 7273 nninfwlpor 7275 nninfwlpoimlemg 7276 nninfwlpoimlemginf 7277 nninfwlpoim 7280 nninfinfwlpo 7281 xaddval 9966 0tonninf 10583 1tonninf 10584 nninfinf 10586 sumeq1 11637 summodc 11665 zsumdc 11666 fsum3 11669 isumss 11673 sumsplitdc 11714 prodeq1f 11834 zproddc 11861 fprodseq 11865 nninfctlemfo 12332 pcmpt 12637 pcmpt2 12638 pcfac 12644 lgsval 15452 lgsneg 15472 lgsdilem 15475 lgsdir2 15481 lgsdir 15483 bj-charfunbi 15709 2omap 15894 subctctexmid 15899 nninfalllem1 15907 nninfsellemdc 15909 nninfself 15912 nninfsellemeq 15913 nninfsellemqall 15914 nninfsellemeqinf 15915 nninfomni 15918 nninffeq 15919 nnnninfex 15921 dceqnconst 15961 dcapnconst 15962 |
| Copyright terms: Public domain | W3C validator |