Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr2d | GIF version |
Description: Deduction form of bitr2i 174. (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 177 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3 | bicomd 129 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3bitrrd 204 3bitr2rd 206 pm5.18dc 777 drex1 1679 elrnmpt1 4585 xpopth 5802 sbcopeq1a 5813 ltnnnq 6521 ltaddsub 7431 leaddsub 7433 posdif 7450 lesub1 7451 ltsub1 7453 lesub0 7474 possumd 7560 ltdivmul 7842 ledivmul 7843 zlem1lt 8300 zltlem1 8301 fzrev2 8947 fz1sbc 8958 elfzp1b 8959 qtri3or 9098 sumsqeq0 9332 sqrtle 9634 sqrtlt 9635 absgt0ap 9695 |
Copyright terms: Public domain | W3C validator |