This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbrbif

Description: Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993) (Revised by Mario Carneiro, 4-Oct-2016)

Ref Expression
Hypotheses sbrbif.1 ⊢ Ⅎ 𝑥 𝜒
sbrbif.2 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
Assertion sbrbif ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 sbrbif.1 ⊢ Ⅎ 𝑥 𝜒
2 sbrbif.2 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
3 2 sbrbis ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) )
4 1 sbf ⊢ ( [ 𝑦 / 𝑥 ] 𝜒 ↔ 𝜒 )
5 4 bibi2i ⊢ ( ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ ( 𝜓 ↔ 𝜒 ) )
6 3 5 bitri ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ 𝜒 ) )