Metamath Proof Explorer


Theorem sbrbis

Description: Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993)

Ref Expression
Hypothesis sbrbis.1 ( [ 𝑦 / 𝑥 ] 𝜑𝜓 )
Assertion sbrbis ( [ 𝑦 / 𝑥 ] ( 𝜑𝜒 ) ↔ ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) )

Proof

Step Hyp Ref Expression
1 sbrbis.1 ( [ 𝑦 / 𝑥 ] 𝜑𝜓 )
2 sbbi ( [ 𝑦 / 𝑥 ] ( 𝜑𝜒 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) )
3 1 bibi1i ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) )
4 2 3 bitri ( [ 𝑦 / 𝑥 ] ( 𝜑𝜒 ) ↔ ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) )