Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sylbb2.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
sylbb2.2 | ⊢ ( 𝜒 ↔ 𝜓 ) | ||
Assertion | sylbb2 | ⊢ ( 𝜑 → 𝜒 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbb2.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
2 | sylbb2.2 | ⊢ ( 𝜒 ↔ 𝜓 ) | |
3 | 2 | biimpri | ⊢ ( 𝜓 → 𝜒 ) |
4 | 1 3 | sylbi | ⊢ ( 𝜑 → 𝜒 ) |