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

Metamath Proof Explorer

Theorem sblbis

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

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

Proof

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