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 878 drex1 1791 elrnmpt1 4862 xpopth 6155 sbcopeq1a 6166 ltnnnq 7385 ltaddsub 8355 leaddsub 8357 posdif 8374 lesub1 8375 ltsub1 8377 lesub0 8398 possumd 8488 subap0 8562 ltdivmul 8792 ledivmul 8793 zlem1lt 9268 zltlem1 9269 negelrp 9644 fzrev2 10041 fz1sbc 10052 elfzp1b 10053 qtri3or 10199 sumsqeq0 10554 sqrtle 11000 sqrtlt 11001 absgt0ap 11063 iser3shft 11309 dvdssubr 11801 gcdn0gt0 11933 divgcdcoprmex 12056 pcfac 12302 lmbrf 13009 logge0b 13605 loggt0b 13606 logle1b 13607 loglt1b 13608 lgsne0 13733 lgsprme0 13737 |
Copyright terms: Public domain | W3C validator |