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 868 drex1 1770 elrnmpt1 4785 xpopth 6067 sbcopeq1a 6078 ltnnnq 7224 ltaddsub 8191 leaddsub 8193 posdif 8210 lesub1 8211 ltsub1 8213 lesub0 8234 possumd 8324 subap0 8398 ltdivmul 8627 ledivmul 8628 zlem1lt 9103 zltlem1 9104 negelrp 9468 fzrev2 9858 fz1sbc 9869 elfzp1b 9870 qtri3or 10013 sumsqeq0 10364 sqrtle 10801 sqrtlt 10802 absgt0ap 10864 iser3shft 11108 dvdssubr 11528 gcdn0gt0 11655 divgcdcoprmex 11772 lmbrf 12373 |
Copyright terms: Public domain | W3C validator |