Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr3g | GIF version |
Description: More general version of 3bitr3i 209. 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 | syl5bbr 193 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
5 | 3, 4 | syl6bb 195 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: con2bidc 860 sbal1yz 1976 sbal1 1977 dfsbcq2 2912 iindif2m 3880 opeqex 4171 rabxfrd 4390 eqbrrdv 4636 eqbrrdiv 4637 opelco2g 4707 opelcnvg 4719 ralrnmpt 5562 rexrnmpt 5563 fliftcnv 5696 eusvobj2 5760 f1od2 6132 ottposg 6152 ercnv 6450 exmidpw 6802 djuf1olem 6938 fzen 9823 fihasheq0 10540 divalgb 11622 isprm3 11799 eldvap 12820 |
Copyright terms: Public domain | W3C validator |