| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > ifbieq1d | GIF version | ||
| Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.) |
| Ref | Expression |
|---|---|
| ifbieq1d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| ifbieq1d.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| ifbieq1d | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ifbieq1d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | ifbid 3594 | . 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶)) |
| 3 | ifbieq1d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 4 | 3 | ifeq1d 3590 | . 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶)) |
| 5 | 2, 4 | eqtrd 2239 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ wb 105 = wceq 1373 ifcif 3573 |
| 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 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-ext 2188 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1485 df-sb 1787 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-rab 2494 df-v 2775 df-un 3172 df-if 3574 |
| This theorem is referenced by: ctssdclemn0 7224 ctssdc 7227 enumctlemm 7228 iseqf1olemfvp 10668 seq3f1olemqsum 10671 seq3f1oleml 10674 seq3f1o 10675 bcval 10907 swrdval 11115 sumrbdclem 11738 summodclem3 11741 summodclem2a 11742 summodc 11744 zsumdc 11745 fsum3 11748 isumss 11752 isumss2 11754 fsum3cvg2 11755 fsum3ser 11758 fsumcl2lem 11759 fsumadd 11767 sumsnf 11770 fsummulc2 11809 isumlessdc 11857 cbvprod 11919 prodrbdclem 11932 prodmodclem3 11936 prodmodclem2a 11937 prodmodc 11939 zproddc 11940 fprodseq 11944 fprodntrivap 11945 prodssdc 11950 fprodmul 11952 prodsnf 11953 pcmpt 12716 pcmptdvds 12718 elply2 15257 lgsval 15531 lgsfvalg 15532 lgsdir 15562 lgsdilem2 15563 lgsdi 15564 lgsne0 15565 |
| Copyright terms: Public domain | W3C validator |