| 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 3591 | . 2 ⊢ ((𝜓 ↔ 𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) | |
| 3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ wb 105 = wceq 1373 ifcif 3571 |
| 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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-11 1529 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-if 3572 |
| This theorem is referenced by: ifbieq1d 3593 ifbieq2d 3595 ifbieq12d 3597 ifandc 3610 ifordc 3611 pw2f1odclem 6931 nnnninf 7228 nnnninf2 7229 nnnninfeq 7230 nninfisollemne 7233 nninfisol 7235 fodjum 7248 fodju0 7249 fodjuomni 7251 fodjumkv 7262 nninfwlporlemd 7274 nninfwlpor 7276 nninfwlpoimlemg 7277 nninfwlpoimlemginf 7278 nninfwlpoim 7281 nninfinfwlpo 7282 xaddval 9967 0tonninf 10585 1tonninf 10586 nninfinf 10588 sumeq1 11666 summodc 11694 zsumdc 11695 fsum3 11698 isumss 11702 sumsplitdc 11743 prodeq1f 11863 zproddc 11890 fprodseq 11894 nninfctlemfo 12361 pcmpt 12666 pcmpt2 12667 pcfac 12673 lgsval 15481 lgsneg 15501 lgsdilem 15504 lgsdir2 15510 lgsdir 15512 bj-charfunbi 15747 2omap 15932 subctctexmid 15937 nninfalllem1 15945 nninfsellemdc 15947 nninfself 15950 nninfsellemeq 15951 nninfsellemqall 15952 nninfsellemeqinf 15953 nninfomni 15956 nninffeq 15957 nnnninfex 15959 dceqnconst 15999 dcapnconst 16000 |
| Copyright terms: Public domain | W3C validator |