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 3536 | . 2 ⊢ ((𝜓 ↔ 𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1342 ifcif 3516 |
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-in1 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-if 3517 |
This theorem is referenced by: ifbieq1d 3538 ifbieq2d 3540 ifbieq12d 3542 ifandc 3552 nnnninf 7082 nnnninf2 7083 nnnninfeq 7084 nninfisollemne 7087 nninfisol 7089 fodjum 7102 fodju0 7103 fodjuomni 7105 fodjumkv 7116 xaddval 9773 0tonninf 10365 1tonninf 10366 sumeq1 11286 summodc 11314 zsumdc 11315 fsum3 11318 isumss 11322 sumsplitdc 11363 prodeq1f 11483 zproddc 11510 fprodseq 11514 pcmpt 12262 pcmpt2 12263 pcfac 12269 bj-charfunbi 13555 subctctexmid 13743 nninfalllem1 13750 nninfsellemdc 13752 nninfself 13755 nninfsellemeq 13756 nninfsellemqall 13757 nninfsellemeqinf 13758 nninfomni 13761 nninffeq 13762 dceqnconst 13800 dcapnconst 13801 |
Copyright terms: Public domain | W3C validator |