Description: Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sbrbis.1 | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) | |
Assertion | sbrbis | ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbrbis.1 | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) | |
2 | sbbi | ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜒 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) ) | |
3 | 1 | bibi1i | ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) ) |
4 | 2 3 | bitri | ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) ) |