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 4860 xpopth 6152 sbcopeq1a 6163 ltnnnq 7372 ltaddsub 8342 leaddsub 8344 posdif 8361 lesub1 8362 ltsub1 8364 lesub0 8385 possumd 8475 subap0 8549 ltdivmul 8779 ledivmul 8780 zlem1lt 9255 zltlem1 9256 negelrp 9631 fzrev2 10028 fz1sbc 10039 elfzp1b 10040 qtri3or 10186 sumsqeq0 10541 sqrtle 10987 sqrtlt 10988 absgt0ap 11050 iser3shft 11296 dvdssubr 11788 gcdn0gt0 11920 divgcdcoprmex 12043 pcfac 12289 lmbrf 12968 logge0b 13564 loggt0b 13565 logle1b 13566 loglt1b 13567 lgsne0 13692 lgsprme0 13696 |
Copyright terms: Public domain | W3C validator |