Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr2id | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr2id.1 | ⊢ (𝜑 ↔ 𝜓) |
bitr2id.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
bitr2id | ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2id.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | bitr2id.2 | . . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
3 | 1, 2 | syl5bb 191 | . 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: bitr3di 194 pm5.17dc 894 dn1dc 949 csbabg 3101 uniiunlem 3226 inimasn 5015 cnvpom 5140 fnresdisj 5292 f1oiso 5788 reldm 6146 mptelixpg 6691 1idprl 7522 1idpru 7523 nndiv 8889 fzn 9967 fz1sbc 10021 metrest 13047 |
Copyright terms: Public domain | W3C validator |