Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6rbb | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6rbb.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
syl6rbb.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
syl6rbb | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6rbb.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | syl6rbb.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
3 | 1, 2 | syl6bb 195 | . 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: syl6rbbr 198 bibif 687 pm5.61 783 oranabs 804 pm5.7dc 938 nbbndc 1372 resopab2 4866 xpcom 5085 f1od2 6132 map1 6706 ac6sfi 6792 elznn0 9072 rexuz3 10765 xrmaxiflemcom 11021 metrest 12678 sincosq3sgn 12912 sincosq4sgn 12913 |
Copyright terms: Public domain | W3C validator |