Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr2d | GIF version |
Description: Deduction form of bitr2i 184. (Contributed by NM, 9-Jun-2004.) |
Ref | Expression |
---|---|
bitr2d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bitr2d.2 | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
bitr2d | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | bitr2d.2 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | |
3 | 1, 2 | bitrd 187 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3 | bicomd 140 | 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: 3bitrrd 214 3bitr2rd 216 pm5.18dc 853 drex1 1754 elrnmpt1 4760 xpopth 6042 sbcopeq1a 6053 ltnnnq 7199 ltaddsub 8166 leaddsub 8168 posdif 8185 lesub1 8186 ltsub1 8188 lesub0 8209 possumd 8299 subap0 8373 ltdivmul 8602 ledivmul 8603 zlem1lt 9078 zltlem1 9079 negelrp 9443 fzrev2 9833 fz1sbc 9844 elfzp1b 9845 qtri3or 9988 sumsqeq0 10339 sqrtle 10776 sqrtlt 10777 absgt0ap 10839 iser3shft 11083 dvdssubr 11466 gcdn0gt0 11593 divgcdcoprmex 11710 lmbrf 12311 |
Copyright terms: Public domain | W3C validator |