![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr3g | GIF version |
Description: More general version of 3bitr3i 210. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.) |
Ref | Expression |
---|---|
3bitr3g.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr3g.2 | ⊢ (𝜓 ↔ 𝜃) |
3bitr3g.3 | ⊢ (𝜒 ↔ 𝜏) |
Ref | Expression |
---|---|
3bitr3g | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3g.2 | . . 3 ⊢ (𝜓 ↔ 𝜃) | |
2 | 3bitr3g.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | bitr3id 194 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
5 | 3, 4 | bitrdi 196 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: con2bidc 875 sbal1yz 2001 sbal1 2002 dfsbcq2 2965 iindif2m 3954 opeqex 4249 rabxfrd 4469 eqbrrdv 4723 eqbrrdiv 4724 opelco2g 4795 opelcnvg 4807 ralrnmpt 5658 rexrnmpt 5659 fliftcnv 5795 eusvobj2 5860 f1od2 6235 ottposg 6255 ercnv 6555 exmidpw 6907 djuf1olem 7051 fzen 10042 fihasheq0 10772 divalgb 11929 isprm3 12117 eldvap 14121 |
Copyright terms: Public domain | W3C validator |