![]() |
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 | bitrid 192 | . 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
4 | 3 | bicomd 141 | 1 ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: bitr3di 195 pm5.17dc 904 dn1dc 960 csbabg 3118 uniiunlem 3244 inimasn 5046 cnvpom 5171 fnresdisj 5326 f1oiso 5826 reldm 6186 mptelixpg 6733 1idprl 7588 1idpru 7589 nndiv 8959 fzn 10041 fz1sbc 10095 grpid 12911 metrest 13976 |
Copyright terms: Public domain | W3C validator |