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 899 dn1dc 955 csbabg 3110 uniiunlem 3236 inimasn 5026 cnvpom 5151 fnresdisj 5306 f1oiso 5802 reldm 6162 mptelixpg 6708 1idprl 7539 1idpru 7540 nndiv 8906 fzn 9985 fz1sbc 10039 metrest 13221 |
Copyright terms: Public domain | W3C validator |