| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > ifbieq2d | GIF version | ||
| Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
| Ref | Expression |
|---|---|
| ifbieq2d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| ifbieq2d.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| ifbieq2d | ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ifbieq2d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | ifbid 3602 | . 2 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴)) |
| 3 | ifbieq2d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 4 | 3 | ifeq2d 3599 | . 2 ⊢ (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵)) |
| 5 | 2, 4 | eqtrd 2240 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ wb 105 = wceq 1373 ifcif 3580 |
| 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 2189 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1485 df-sb 1787 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-rab 2495 df-v 2779 df-un 3179 df-if 3581 |
| This theorem is referenced by: difinfsnlem 7229 ctmlemr 7238 xnegeq 9986 xaddval 10004 iseqf1olemqval 10684 iseqf1olemqk 10691 seq3f1olemqsum 10697 exp3val 10725 gcdval 12441 gcdass 12497 lcmval 12546 lcmass 12568 pcval 12780 ennnfonelemj0 12933 ennnfonelemjn 12934 ennnfonelem0 12937 ennnfonelemp1 12938 ennnfonelemnn0 12954 mulgval 13619 znval 14559 lgsval 15642 lgsfvalg 15643 lgsval2lem 15648 nnsf 16252 peano4nninf 16253 peano3nninf 16254 exmidsbthr 16272 |
| Copyright terms: Public domain | W3C validator |