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 ⊢ Ⅎ x χ
sbrbif.2 ⊢ y x φ ↔ ψ
Assertion sbrbif ⊢ y x φ ↔ χ ↔ ψ ↔ χ

Proof

Step Hyp Ref Expression
1 sbrbif.1 ⊢ Ⅎ x χ
2 sbrbif.2 ⊢ y x φ ↔ ψ
3 2 sbrbis ⊢ y x φ ↔ χ ↔ ψ ↔ y x χ
4 1 sbf ⊢ y x χ ↔ χ
5 4 bibi2i ⊢ ψ ↔ y x χ ↔ ψ ↔ χ
6 3 5 bitri ⊢ y x φ ↔ χ ↔ ψ ↔ χ