Metamath Proof Explorer

Theorem sbrbis

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

Ref Expression
Hypothesis sbrbis.1 ⊢ y x φ ↔ ψ
Assertion sbrbis ⊢ y x φ ↔ χ ↔ ψ ↔ y x χ

Proof

Step Hyp Ref Expression
1 sbrbis.1 ⊢ y x φ ↔ ψ
2 sbbi ⊢ y x φ ↔ χ ↔ y x φ ↔ y x χ
3 1 bibi1i ⊢ y x φ ↔ y x χ ↔ ψ ↔ y x χ
4 2 3 bitri ⊢ y x φ ↔ χ ↔ ψ ↔ y x χ