Metamath Proof Explorer

Theorem sb3an

Description: Threefold conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006)

Ref Expression
Assertion sb3an ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ y x ψ ∧ y x χ

Proof

Step Hyp Ref Expression
1 sban ⊢ y x φ ∧ ψ ↔ y x φ ∧ y x ψ
2 1 anbi1i ⊢ y x φ ∧ ψ ∧ y x χ ↔ y x φ ∧ y x ψ ∧ y x χ
3 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
4 3 sbbii ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ ψ ∧ χ
5 sban ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ ψ ∧ y x χ
6 4 5 bitri ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ ψ ∧ y x χ
7 df-3an ⊢ y x φ ∧ y x ψ ∧ y x χ ↔ y x φ ∧ y x ψ ∧ y x χ
8 2 6 7 3bitr4i ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ y x ψ ∧ y x χ