Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bibi2i.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
Assertion | bibi1i | ⊢ ( ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bibi2i.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
2 | bicom | ⊢ ( ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜒 ↔ 𝜑 ) ) | |
3 | 1 | bibi2i | ⊢ ( ( 𝜒 ↔ 𝜑 ) ↔ ( 𝜒 ↔ 𝜓 ) ) |
4 | bicom | ⊢ ( ( 𝜒 ↔ 𝜓 ) ↔ ( 𝜓 ↔ 𝜒 ) ) | |
5 | 2 3 4 | 3bitri | ⊢ ( ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ 𝜒 ) ) |