| 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 3624 | . 2 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴)) |
| 3 | ifbieq2d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 4 | 3 | ifeq2d 3621 | . 2 ⊢ (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵)) |
| 5 | 2, 4 | eqtrd 2262 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ wb 105 = wceq 1395 ifcif 3602 |
| 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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-ext 2211 |
| This theorem depends on definitions: df-bi 117 df-tru 1398 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-rab 2517 df-v 2801 df-un 3201 df-if 3603 |
| This theorem is referenced by: difinfsnlem 7282 ctmlemr 7291 xnegeq 10040 xaddval 10058 iseqf1olemqval 10739 iseqf1olemqk 10746 seq3f1olemqsum 10752 exp3val 10780 gcdval 12501 gcdass 12557 lcmval 12606 lcmass 12628 pcval 12840 ennnfonelemj0 12993 ennnfonelemjn 12994 ennnfonelem0 12997 ennnfonelemp1 12998 ennnfonelemnn0 13014 mulgval 13680 znval 14621 lgsval 15704 lgsfvalg 15705 lgsval2lem 15710 nnsf 16485 peano4nninf 16486 peano3nninf 16487 exmidsbthr 16505 |
| Copyright terms: Public domain | W3C validator |