![]() |
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 2966 iindif2m 3955 opeqex 4250 rabxfrd 4470 eqbrrdv 4724 eqbrrdiv 4725 opelco2g 4796 opelcnvg 4808 ralrnmpt 5659 rexrnmpt 5660 fliftcnv 5796 eusvobj2 5861 f1od2 6236 ottposg 6256 ercnv 6556 exmidpw 6908 djuf1olem 7052 fzen 10043 fihasheq0 10773 divalgb 11930 isprm3 12118 eldvap 14154 |
Copyright terms: Public domain | W3C validator |